% $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
%
see also: discovery notes 23 Sep 2003
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.