Self-application is the application of a term to (a copy of) itself. Here are two examples:
- $(\lambda x . x)(\lambda x. x)$
- $(\lambda x . x x)(\lambda x . x x)$
The first examples applies the identity function $\lambda x . x$ to itself. It reduces in one step to the identity function, which is in normal form.
The second example applies the self-application function $\lambda x. x x$ to itself. It reduces in one step to a copy of the second example, which reduces in one step to a copy of the second example, etc. So this is an example of a nonterminating computation.
You are right that fixed-point combinators are another class of examples.
In the simply typed lambda calculus, the term $\lambda x . x x$ is ill-typed because we have to assign the same type to both bound occurrences of $x$. If we assign type $A$ to the second occurrence, we have to assign type $A \to A$ to the first occurrence to make the term well-typed. But $A$ and $A \to A$ cannot be the same, so the term cannot be well-typed.
Note that just because the second example is non-terminating in the untyped lambda-calculus, and ill-typed in the simply-typed lambda-calculus, doesn't mean it's not "valid". Many valid computer programs can have non-terminating behavior on purpose or by necessity, and maybe we want a mathematical theory of computation to model such programs. For example, a Web browser should only terminates if the user closes the window, but if the user never closes it, the browser should keep running forever.
This is an interesting difference between theories of truth (as in mathematical logic) and theories of computation (as in theoretical computer science): In a theory of truth, if something is not a valid proof of some truth, we don't really care for details. But in a theory of computation, if something doesn't terminate, we still might want to investigate the computational behavior that is shown while not terminating.
Truth table semantics is particular to classical propositional logic. So if the author were being specific, they would have added this qualifier. (However it’s probably a good rule of thumb that if you just see “propositional calculus,” in most contexts they are referring to classical.)
While “propositional” is a descriptor that mainly refers to the language (in particular, the absence of non logical symbols other than sentence letters), as soon as we start talking about proof systems or semantics, we have a particular logic in mind: classical, intuistionistic, minimal, modal, etc.
Best Answer
Proof theoretically intuitionist logic is a sub-theory of classical logic. The Wikipedia article indicates this by indicating that if we have a certain set of axioms for intuitionist logic (those axioms can get found under the section entitled "Hilbert style calculus", then classical logic may get obtained by joining to the system the law of the excluded middle... in Polish notation ApNp, Peirce's law CCCpqpp, or the law of double negation elimination CNNpp, or with the definition Np := Cp0, we might write CCCp00p.
Thus, all formal proofs done in a an intuitionist logic framework work as proofs for any classical logic framework, but not all proofs done in a classical logic framework will work in any intuitionist logic framework.
For example, one might deduce Cpp from a classical logic framework as follows:
This is not a possible proof of Cpp in any intuitionist logic framework, since CCNppp is not a thesis in any intuitionist logic (the term "thesis" refers to a formula which is either an axiom or a theorem).
Semantically speaking intuitionist logic qualifies as much richer than classical logic in that the truth set for intuitionist logic is infinite-valued, while that of classical logic is two-valued. Semantically speaking, intuitionist logic behaves the same way as classical logic when truth-values get confined to "True" and "False". In such a case, each formula whether interpreted from the perspective of classical logic or intuitionist logic yields the same result. But, intuitionist logic can get said to reject the law of bivalence in that no two-valued models of intuitionist logic qualify as adequate for a semantics of it.