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

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.