Logical Theory
The following functions are introduced.
-
sta(X) converts a set of sequents X to a set of
assertions
sta ≝ λX.{<{},s> |
s ∈ X}
-
dta(X) converts a set of deductions X to a set of
assertions
dta ≝ λX.{r | <r,p>
∈ X}
-
les(X,x) returns all elements of an ordered set X less than some element x
grt ≝ λX.λx.{y | y
∈ X ∧ y < x}
-
grt(X,x) returns all elements of an ordered set X greater than some element x
grt ≝ λX.λx.{y | y
∈ X ∧ y > x}
-
sga(X,x) returns all sequents of an ordered set of
sequents X greater than some
sequent x as assertions
sga ≝ λX.λx.sta(grt(X,x))
-
ats(X) returns the set of all sequents in the set of
assertions X
ats ≝
λX.{⊨x | ⊨x ∈ X}
-
stc(X) returns the set of all conclusions in a set
of sequents X
stc ≝
λX.{s | <r,s> ∈ X}
-
stp(X) returns the union of all premises in a set of
sequents X
stp ≝
λX.{x | <r,s> ∈ X ∧ x ∈ r}
If F is a set of functions from elements of W to elements of W then
-
gts ≝
λF.{λP ⊢ t . {f(x) | x ∈ P} ⊢ f(t) | f ∈ F}
-
gta ≝
λF.{λA ⊨ s . {f(x) | x ∈ A} ⊨ f(s) | f ∈ gts(F)}
where an element of gts(F) is called a global transformation function
of sequents of W and an element of gta(F) is called a
global transformation function of
assertions of W.
If F is a set of functions from elements of W to elements of W then
-
lxs ≝
λf.λx.λP.{z | ∃y.y ∈ P ∧
((x = y ∧ z = f(y)) ∨ (x ≠ y ∧ z = y))}
-
lts ≝
λF.({λP ⊢ t.lxs(f,x,P) ⊢ t | x ∈
W ∧ f ∈ F} ∪ {λP ⊢ t.P ⊢ f(t) | f ∈ F})
-
lta ≝
λF.({λA ⊨ s.lxs(f,x,A) ⊨ s | x ∈ W ∧ f ∈
lts(F)} ∪ {λA ⊨ s.A ⊨ f(s) | f ∈ lts(F)})
where an element of lts(F) is called a local transformation function of
sequents of W and an element of lta(F) is called a
local transformation function of assertions
of W.
Let W be a set. A transformation structure on W is a set of
functions from assertions of W to
assertions of W such that the set contains the identity
function and which is closed under function composition. Such a set forms a
monoid under function composition. The smallest transformation structure on W
contains only the identity function and the largest contains all functions.
An assertion x is said to precede an
assertion y if there is a function f in the
transformation structure on W such that f(x) = y and is written x ≾ y.
Alternatively, y is said to be an instance of x. If x ≾
y and y ≾ x then x is said to be equivalent to y and is written x ≈ y.
If x ≾ y and it is not the case that y ≾ x then x is said to strictly
precede y and is written x ≺ y. The ≾ relation is reflexive,
transitive and anti-symmetric under function composition. The ≈ relation
is reflexive, transitive and symmetric under function composition. The ≺
relation is irreflexive and transitive under function composition.
Let W be a set, L a set of functions from W to W and G a set of functions from W to
W where both L and G contain the identity function. Then the transformation
structure defined on W by L and G is the transitive closure under function
composition of gta(G) ∪ lta(L).
Let W be a set, R a set of assertions of W and S a
transformation structure on W. Then a set of sequents
p is well-formed with respect to R and S if p is well-ordered (i.e.
linearly ordered with a minimal element) and for all s ∈ p either
-
there exists an assertion (⊨ Q ⊢ t), a
sequent b ∈ (ats(R) ∪ grt(p,s))
and a set of sequents X ⊆ (ats(R) ∪
grt(p,s))where b ≾ (⊨ Q ⊢ t)
and s = ((Q - stc(X)) ∪ stp(X)) ⊢ t.
-
there exists an assertion (B ⊨ s) and an
assertion b ∈ (R ∪ sga(p,s))
where b ≾ (B ⊨ s) and B ⊆ (ats(R) ∪ grt(p,s)).
Let W be a set, R a set of assertions of W, S a
transformation structure on W and <B,s> an assertion
of W. Then a set of sequents p is a proof
of <B,s> with respect to R and S if p is well-formed with respect to
(R ∪ sta(B)) and S such that s is the minimal sequent
in p and where the omission of any sequent in p or the
omission of any assumption in B would result in p not
being well-formed with respect to (R ∪ sta(B)) and S.
Let W be a set, S a transformation structure on W and R a set of
assertions of W. Then a deduction of W
with respect to R and S is a tuple <r,p> where r is an
assertion of W and p is a proof
of r with respect to R and S.
A logical theory is a tuple <W,L,G,A,T> where
-
W is a set of words. The elements of W are also called
terms, formulae, sentences and
statements.
-
L is a set of functions from W to W which contains the identity function. An
element of L is called a local transformation function of W. L
represents renaming of bound variables and replacement of defined constants.
It also represents the equivalence of terms which differ by the addition or
removal of parentheses and of other purely syntatic transformations.
-
G is a set of functions from W to W which contains the identity function. An
element of G is called a global transformation function of W. G
represents renaming of unbound variables and substitution of terms. An element
t of W is said to be closed if for all f ∈ G, t = f(t) and is
otherwise said to be open.
-
A is a set of assertions of W. A represents
the set of assumptions. For all <B,s> ∈ A if B = ∅ then
<B,s> is an axiom and is otherwise a rule.
-
T is a well-ordered set of tuples <r,p> where r is an
assertion of W and p is a set of
sequents of W such that for all t ∈ T,
t is a deduction of W with respect to (A ∪ dta(les(T,t))) and S,
where S is the transformation structure defined on W by G and L.
T represents the set of consequences. For all <<B,s>,p>
∈ T if B = ∅ then <<B,s>,p> is a theorem
and is otherwise a derived rule.
If L is a logical theory then a sequent of L is defined as a
sequent of W, an assertion
of L is defined as an assertion of W and a deduction of
L is defined as a deduction of W with respect to (A ∪ dta(T)) and S. For
a logical theory, the terms are defined by its formative rules and the transformation
functions are defined by its transformational rules.
A logical theory is standard when terms are composed of finite strings
of symbols not including ⊢ and ⊨, all sequents,
assertions and proofs contain only finite sets, the set
of consequences is finite and when
hold in the system so that ⊢ satisifies
the necessary conditions to be a consequence relation. If
reflexivity is available as an axiom or theorem then monotonicity and transitivity
can be proven as derived meta-rules.
-
monotonicity meta-rule
(P ⊢ s)
⊨
(P ∪ {r} ⊢ s)
Proof:
| 1.
| {r} ⊢ r
|
| axiom or theorem
|
| 2.
| P ∪ {r} ⊢ s
|
| apply P ⊢ s to get (P - {r}) ∪ {r} ⊢ s
|
-
transitivity meta-rule
(P ⊢ r),
(P ∪ {r} ⊢ s)
⊨
(P ⊢ s)
Proof:
| 1.
| P ⊢ s
|
| apply P ∪ {r} ⊢ s to get ((P ∪ {r}) - {r}) ∪ P ⊢ s
|
The reflexivity rule holds in the system.
The transformation meta- rule holds in the system
{p} ⊨ q [p ≾ q]
Proof:
| 1.
| q
|
| assumption where p ≾ q
|
[ Last | Overview ]