A language L for Arithmetic. The judgement tree.

We replace, in the language L of the previous sections, material implication → with constructive implication ⇒.

The Language LCons. We consider the language LCons for arithmetic, having one constant symbol n for each natural number, one predicate symbol p for each computable predicate, one function symbol f for each computable function. Formulas are all first order formulas in the logical constant T, F, and the connectives ∧, ∨, ⇒, ⊃ (two version of constructive implication, see below), ¬, and ∀, ∃ (with quantifiers ranging over natural numbers).
A judgement is a statement t.A or f.A, to be read: ``A is true'', ``A is false''. We call t., f. the sign of the judgment. t. is a positive sign and t.A a positive judgment. f.A is a negative sign and f.A a negative judgement.

Constructive Implication (⇒). In LCons, negation and implication are constructive negation and implication. The intended meaning of ¬A is: ``in all possible worlds, if we assume A we derive a contradiction''. In LCons, we write implication as A⇒B, instead of A→B (we use A→B to denote material implication). The semantic of ``A⇒B'' is: ``in all possible worlds, if we assume A we derive B''. The operational meaning of A⇒B is: ``there is an effective way of taking any evidence in favor of A, and turning it into an evidence in favor of B''. A→B (material implication) and A⇒B are equivalent if we have full classical logic, but many proofs (even many classical proofs) are easier to follow if we take the constructive meaning of negation and implication. This is why we will also consider game semantic for constructive negation and implication.

The connective ``if'' (⊃). We abbreviate: ``if we assume A we derive B'' by A⊃B. We call the new connective ⊃: ``if ... then else ...'', or just ``if'' for short.  
With this abbreviation, A⇒B now means: ``in all possible worlds, A⊃B''. We assimilate the quantification on all possible worlds to a conjuction. Therefore we identify with A⇒B the unary conjunction of A⊃B. We think of A⊃B as some kind of disjunction, because it is intuitionistically implied by (and classically equivalent to): ``either A is false, or B is true''.

The difference between ⇒ and ⊃. We think of A⇒B as the sound and complete interpretation of constructive implication. The formula A⊃B is just a step in the interpretation of A⇒B. The formulas A⇒B and A⊃B are equivalent modulo some (quite weak) structural rules of logic.

Subjudgements. If A is closed, the immediate subjudgements of t.A or f.A are the following.
1. T, F have no immediate subjudgements.
2. t.a and f.a, with a atomic have immediate subjudgement t.T and f.T if a is true, have immediate subjudgement t.F and f.F if a is false.
3. t.A∧B, t.A∨B have immediate subjudgements t.A, t.B. f.A∧B, f.A∨B have immediate subjudgements f.A, f.B.
*4. t.A⇒B has immediate subjudgement t.A⊃B, and f.A⇒B has immediate subjudgement f.A⊃B.
*5. t.A⊃B has immediate subjudgements f.A, t.B, and f.A⊃B has immediate subjudgements t.A, f.B.
6.  t.¬A has immediate subjudgement f.A, f.¬A has immediate subjudgements t.A.
7. t.∀x.A, t.∃x.A have immediate subjudgements t.A[t/x], for all closed terms t. f.∀x.A, f.∃x.A have immediate subjudgements f.A[t/x], for all closed t.
The subjudgements of of t.A or f.A are all immediate subjudgements, all immediate subjudgements of all immediate subjudgements, and so forth.

Judgement tree. The judgement tree of t.A (or f.A) is the tree having nodes the subjudgements of t.A (or f.A), and edges representing the relation: ``immediate subjudgement''. The judgement tree of A is the judgement tree of t.A.

This is the judgement tree of t.∃x.∀y.P(x,y)⇒∃x.(P(x,b)∧P(x,c)), in which, for simplicity, we draw only one subjudgement for each quantifier, and we cut down the tree to the nodes of the form P(x,y):

Created by Mathematica  (November 11, 2006)