Editing Natural deduction (section)

==First and higher-order extensions==
{{Unreferenced section|date=May 2024}}
[[File:first order natural deduction.png|thumb|right|Summary of first-order system]]

The logic of the earlier section is an example of a ''single-sorted'' logic, ''i.e.'', a logic with a single kind of object: propositions. Many extensions of this simple framework have been proposed; in this section we will extend it with a second sort of ''individuals'' or ''[[term (logic)|terms]]''. More precisely, we will add a new category, "term", denoted <math>\mathcal{T}</math>. We shall fix a [[countable]] set ''<math>V</math>'' of ''variables'', another countable set <math>F</math> of ''function symbols'', and construct terms with the following formation rules:

:<math>
\frac{v\in V}{v : \mathcal{T}} \hbox{ var}_F
</math>

and
:<math>
\frac{f\in F\qquad t_1 : \mathcal{T}\qquad   t_2 : \mathcal{T}\qquad \cdots \qquad t_n : \mathcal{T}}{f(t_1, t_2,\cdots,t_n) : \mathcal{T}} \hbox{ app}_F
</math>

For propositions, we consider a third countable set ''P'' of ''[[Predicate (mathematical logic)|predicates]]'', and define ''atomic predicates over terms'' with the following formation rule:

:<math>
\frac{\phi\in P\qquad t_1 : \mathcal{T}\qquad   t_2 : \mathcal{T}\qquad \cdots \qquad t_n : \mathcal{T}}{\phi(t_1, t_2,\cdots,t_n) : \mathcal{F}} \hbox{ pred}_F
</math>

The first two rules of formation provide a definition of a term that is effectively the same as that defined in [[term algebra]] and [[model theory]], although the focus of those fields of study is quite different from natural deduction. The third rule of formation effectively defines an [[atomic formula]], as in [[first-order logic]], and again in model theory.

To these are added a pair of formation rules, defining the notation for ''[[quantifier (logic)|quantified]]'' propositions; one for universal (∀) and existential (∃) quantification:

:<math>
\frac{x\in V \qquad A : \mathcal{F}}{\forall x.A : \mathcal{F}} \;\forall_F
\qquad\qquad
\frac{x\in V \qquad A : \mathcal{F}}{\exists x.A : \mathcal{F}} \;\exists_F
</math>

The [[universal quantifier]] has the introduction and elimination rules:

:<math>

\cfrac{
\begin{array}{c}
\cfrac{}{a : \mathcal{T}}\text{ u}
\\ \vdots
\\{}[a/x]A 
\end{array}
}{\forall x.A }\;\forall_{I^{u,a}}
\qquad \qquad
\frac{\forall x.A \qquad t : \mathcal{T}}{[t/x]A}\;\forall_{E}
</math>

The [[existential quantifier]] has the introduction and elimination rules:
:<math>
\frac{[t/x]A }{\exists x.A}\;\exists_{I}
\qquad\qquad
\cfrac{
\begin{array}{cc}
& \underbrace{\,\cfrac{}{a : \mathcal{T}}\hbox{ u} \quad \cfrac{}{[a/x]A }\hbox{ v}\,}\\
& \vdots \\
\exists x.A \quad & C \\
\end{array}
}
{C }\exists_{E^{a,u,v}}
</math>

In these rules, the notation [''t''/''x''] ''A'' stands for the substitution of ''t'' for every (visible) instance of ''x'' in ''A'', avoiding capture.{{refn|See the article on [[lambda calculus]] for more detail about the concept of substitution.}} As before the superscripts on the name stand for the components that are discharged: the term ''a'' cannot occur in the conclusion of ∀I (such terms are known as ''eigenvariables'' or ''parameters''), and the hypotheses named ''u'' and ''v'' in ∃E are localised to the second premise in a hypothetical derivation. Although the propositional logic of earlier sections was [[Decidability (logic)|decidable]], adding the quantifiers makes the logic undecidable.

So far, the quantified extensions are ''first-order'': they distinguish propositions from the kinds of objects quantified over. [[Higher-order logic]] takes a different approach and has only a single sort of propositions. The quantifiers have as the domain of quantification the very same sort of propositions, as reflected in the formation rules:

:<math>
\cfrac{
\begin{matrix}
\cfrac{}{p : \mathcal{F}}\hbox{ u} \\
\vdots \\
A: \mathcal{F} \\
\end{matrix}}
{\forall p.A : \mathcal{F}} \;\forall_{F^u}
\qquad\qquad

\cfrac{
\begin{matrix}
\cfrac{}{p : \mathcal{F}}\hbox{ u} \\
\vdots \\
A: \mathcal{F} \\
\end{matrix}}
{\exists p.A : \mathcal{F}} \;\exists_{F^u}
</math>

A discussion of the introduction and elimination forms for higher-order logic is beyond the scope of this article. It is possible to be in-between first-order and higher-order logics. For example, [[second-order logic]] has two kinds of propositions, one kind quantifying over terms, and the second kind quantifying over propositions of the first kind.