% $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.