% \$Id: LogicOfProofs.html,v 1.2 2003/10/03 21:02:07 connolly Exp \$
%
% based on
S. Artemov, Explicit provability and constructive semantics, Bulletin of Symbolic Logic, volume 7, No.1, pp. 1-36, 2001 %
LogicOfProofs: trait
includes
FormalSystem,
Set(ProofPoly, FiniteSet[ProofPoly] for Set[E])

introduces
LP0, LP : → System
[ __ ] : ProofVar → ProofPoly
[ __ ] : ProofConstant → ProofPoly
! __  : ProofPoly → ProofPoly
__ * __ : ProofPoly, ProofPoly → ProofPoly
__ + __ : ProofPoly, ProofPoly → ProofPoly

⊤ : → Formula % truth
⊥ : → Formula % absurdity/false
[ __ ] : PropLetter → Formula
__ ⇒ __ : Formula, Formula → Formula
__ ∧ __ : Formula, Formula → Formula
__ ∨ __ : Formula, Formula → Formula
\not __ : Formula → Formula
__ / __: ProofPoly, Formula → Formula
__ / __: FiniteSet[ProofPoly], Set[Formula] → Set[Formula]

ModusPonens : → Rule
Necessitation : → Rule

% @@ /\, \/ over finite sets of formulas

asserts
%@@ProofPoly generated by v, c, !, *, +
∀ F, G, A: Formula, s, t: ProofPoly, c: ProofConstant

% @@ [A0] Finite set of axiom schemes of classical propositional logic

% [A1] reflection
axiom(LP0, (t/F) ⇒ F);

% [A2] "application"
axiom(LP0, (t/(F ⇒ G)) ⇒ ((s/F) ⇒ ((t*s)/G)));

% [A3] "proof checker"
axiom(LP0, (t/F) ⇒ ((!t)/(t/F)));

% [A4] "sum"
axiom(LP0, (s/F) ⇒ ((s+t)/F));
axiom(LP0, (t/F) ⇒ ((s+t)/F));

%Rule of inference:

%[R1] "modus ponens"
direct_consequence(LP0, ModusPonens, insert(F ⇒ G, {F}), G);

% LP is just like LP0 but for one rule... hmm...
axiom(LP0, F) ⇒ axiom(LP, F);
axiom(LP0, A) ⇒
direct_consequence(LP, Necessitation, {A}, [c]/A);

implies
∀ GAMMA, DELTA: Set[Formula], A, B, F: Formula,
ss: FiniteSet[ProofPoly]

% deduction theorem
% hmm... GAMMA, DELTA should be finite
deducible(LP0, GAMMA ∪ {A}, B) ⇒
deducible(LP0, GAMMA, A ⇒ B);

% lifting lemma
deducible(LP, (ss/GAMMA) ∪ DELTA, F); %@@ more

[Index]

HTML generated using lsl2html.