% $Id: FormalSystem.lsl,v 1.4 2003/10/01 07:25:52 connolly Exp $

% A transcription of
%
%html <a href="http://www-rci.rutgers.edu/~cfs/305_html/Deduction/FormalSystemDefs.html">Formal Systems - Definitions</a>
% (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
        \forall T: System, Ri: Rule, S: Set[Formula], A, f, P: Formula,
	        Sf: FiniteSet[Formula], Pi: List[Formula]

        wff(T, S) /\ f \in 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 \in Sf => wff(T, f);

	proof(T, S, P, Pi) = (
	    (last(Pi) = P)
	    /\ (axiom(T, P)
	        \/ P \in S
	        \/ \E Ri \E Sf (Ri \in 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) = \E Pi (proof(T, S, P, Pi));

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

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

	interpret(T, I, f) => wff(T, f);

	model(T, I, S) = \A f (wff(T, f) /\ f \in S => interpret(T, I, f));

	complete(T) = \A f ( (\A I interpret(T, I, f))
			     => theorem(T, f) );

	sound(T) = \A f ( theorem(T, f) => (\A I interpret(T, I, f)));

	consistent(T) = \not \E f ( theorem(T, f) /\ theorem(T, negation(T, f)));

    implies
        \forall 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.