% $Id: FormalSystem.html,v 1.2 2003/10/01 07:26:24 connolly Exp $

% A transcription of
%
Formal Systems - Definitions % (from Ruth E. Davis, Truth, Deduction, and Computation.
% New York: Computer Science press, 1989.)
%
% (c) Charles F. Schmidt
% Last Modified: Saturday, May 08, 1999 9:07:08 PM GMT

FormalSystem: trait
    includes
        CoerceContainer(List[Formula], FiniteSet[Formula], Formula for E),
        RelSet(Formula, Set[Formula]),
        Set(Formula, FiniteSet[Formula] for Set[E]),
        Set(Rule, FiniteSet[Rule] for Set[E]),
        List(Formula),
        Relation(Formula, Rel[Formula])

    introduces

% do this as a tuple?
        wff: System, Formula → Bool
        wff: System, Set[Formula] → Bool
        axiom: System, Formula → Bool
        rules: System → FiniteSet[Rule]
        negation: System, Formula → Formula

        arity: Rule → Int % positive

        direct_consequence: System, Rule, FiniteSet[Formula], Formula → Bool
% for direct_consequence(T, Ri, S, A) read
% A is a direct consequence of S by virtue of Ri in T.

        deducible: System, Set[Formula], Formula → Bool
% for deducible(T, S, P) read P is deducible from S in T.

        proof: System, Set[Formula], Formula, List[Formula] → Bool
% for proof(T, S, P, Pi) read Pi is a proof of P from S in T.

        theorem: System, Formula → Bool
% for theorem(T, P) read P is a theorem (or: is provable) in T

        interpret: System, Interpretation, Formula → Bool
        model: System, Interpretation, Set[Formula] → Bool

        complete: System → Bool
        sound: System → Bool
        consistent: System → Bool

%@@compactness, etc.

    asserts
        ∀ T: System, Ri: Rule, S: Set[Formula], A, f, P: Formula,
                Sf: FiniteSet[Formula], Pi: List[Formula]

        wff(T, S) ∧ f ∈ S ⇒ wff(T, f); %@@ do we need the only if rule?

        arity(Ri) > 0;

        axiom(T, A) ⇒ wff(T, A);

        direct_consequence(T, Ri, Sf, A) ⇒ size(Sf) = arity(Ri);
        direct_consequence(T, Ri, Sf, A) ∧ f ∈ Sf ⇒ wff(T, f);

        proof(T, S, P, Pi) = (
            (last(Pi) = P)
            ∧ (axiom(T, P)
                ∨ P ∈ S
                ∨ ∃ Ri ∃ Sf (Ri ∈ rules(T)
                                ∧ Sf \subset coerce(Pi)
                                ∧ direct_consequence(T, Ri, Sf, P)
                                ∧ (init(Pi) = empty
                                    ∨ proof(T, S, last(init(Pi)), init(Pi)) )
                                    ) ) );

        deducible(T, S, P) = ∃ Pi (proof(T, S, P, Pi));

        theorem(T, P) = deducible(T, {}, P);

        ∀ T: System, I: Interpretation, S: Set[Formula], f: Formula,
                Pi: List[Formula]

        interpret(T, I, f) ⇒ wff(T, f);

        model(T, I, S) = ∀ f (wff(T, f) ∧ f ∈ S ⇒ interpret(T, I, f));

        complete(T) = ∀ f ( (∀ I interpret(T, I, f))
                             ⇒ theorem(T, f) );

        sound(T) = ∀ f ( theorem(T, f) ⇒ (∀ I interpret(T, I, f)));

        consistent(T) = \not ∃ f ( theorem(T, f) ∧ theorem(T, negation(T, f)));

    implies
        ∀ S1, S2: Set[Formula], A: Formula, T: System

% monotonicity
        wff(T, S1)
        ∧ wff(T, S2)
        ∧ wff(T, A)
        ⇒ (S1 \subset S2 ∧ deducible(T, S1, A) ⇒ deducible(T, S2, A));

%@@compactness, etc.

[Index]

HTML generated using lsl2html.