Wires and pipes
Alessio Guglielmi <Alessio.Guglielmi-r/[email protected]>
| Newsgroups | gmane.science.mathematics.frogs |
|---|---|
| Message-ID | <[email protected]> |
Hello,
in this message I propose a formalism and a deductive system for
classical propositional logic.
The formalism, which I'd like to call `wired deduction' (weird
deduction!) should be the first example of deductive derivation net:
it is an intrinsically bureaucracy-free, deductive and geometric
formalism. It naturally subsumes CoS and formalisms A and B.
As usual, I will define the formalism by way of a deductive system,
and the natural choice is classical propositional logic. It is
possible to define the formalism in isolation, in two ways: 1)
geometrically, as a set of graph-forming rules; 2) deductively, by
the definition for formalism B I showed at the workshop, *enriched by
wires* (see below for what wires are).
These definitions are almost trivial after you see a deductive
system. Before posting their details, I would like to receive some
reactions about the deductive system, which you find below.
This email has three parts: Motivations, Intuition and
Technicalities. Reading up to Intuition should be enough to get a
good idea, if you know already about CoS and KS.
I would be very grateful if somebody checks the technicalities,
though. They are nontrivial and unfortunately very combinatorial.
Clearly, they might be wrong, but it should be possible to fix any
mistake without changing the general picture.
Please, if you check, let me know, even if you find no mistakes
(positive information is still very useful!).
Ciao,
-Alessio
MOTIVATION
==========
The general motivation is devising a formalism which is
bureaucracy-free and *intrinsically* so. Moreover, we want the
formalism to be geometric.
Bureaucracy-free means that it should be possible to express, inside
the formalism, canonical representatives of derivations which are
`morally the same' according to some notion. See the message
<http://article.gmane.org/gmane.science.mathematics.frogs/219>
for an exposition of these ideas. See also the notes
<http://iccl.tu-dresden.de/~guglielm/p/AG11.pdf> ,
<http://iccl.tu-dresden.de/~guglielm/p/AG13.pdf> ,
<http://www.iam.unibe.ch/~kai/Current/prty.pdf> .
`Intrinsically' bureaucracy-free means that the formalism disallows
the very formation of some redundant derivations. This notion is
closely related, somehow, to the idea that the formalism should be
geometric.
For a formalism, being `geometric' means that derivations are some
sort of graphs over which one operates locally and modulo some basic
symmetries like those due to commutativity and associativity.
Much of the inspiration for wired deduction comes from subatomic
logic, especially the idea of wires and the ww_ rule. See
<http://iccl.tu-dresden.de/~guglielm/p/AG8.pdf> .
In the design of the deductive system for classical logic, I wanted
to get rid once and for all of the unit equations. They have no
strong justification in terms of `war to bureaucracy' and they cause
some technical problems. I think that the system below is
particularly convincing in this respect. It might be possible to do
better than I did, in the sense that some technicalities can perhaps
be simplified.
INTUITION
=========
I will attempt here a completely informal exposition of the system
for classical logic, called KSw, which should be sufficient for
people who know CoS and KS. The technical definitions are in the
Technicalities part of this message (they are still subject to
changes, of course).
We need to operate under associativity and commutativity, in order to
get rid of bureaucracy in formulae. However, in some cases we need to
keep track of `where the atoms come from'. The obvious solution would
be to disambiguate these situations by resorting to occurrences.
Wires go one step further: they allow following atoms and their
transformations throughout a whole derivation.
The main idea goes as follows: there is a denumerable set of wires.
Wires are neither created nor destroyed. To wires we associate atoms,
and the association may vary in the course of the derivation.
Moreover, at any given time bunches of wires are organised into a
tree of logical relations, which also can change over time. For
example, the following is a derivation of a from (a V a) (so, it's a
contraction):
[a a]
| |
[a f] .
1 2
There are two wires, 1 and 2, vertically disposed, and we assume that
time flows vertically going upwards. In the beginning, a is
associated to 1 and f is associated to 2. In traditional logic, a
would be a propositional variable and f would be the `false' unit;
both are atoms for us. Wires 1 and 2 are in a disjunction relation
(indicated as usual in CoS). After some time wire 2 gets the value a,
but the logical relation between wires does not change. We indicate
this situation by the rule
[a a]
wc_ -|-|- ,
[a f]
which is of course supposed to apply in the middle of other wires.
This is an example of atomic rule. A special feature of wired
deduction is that atomic rules only work on wires, their values and
their relations, by `going through' a predetermined amount of them
(in the case above, two). Atomic rules `see' which atoms wires carry.
There is another kind of rule, the local rule. These are different
than atomic rules, they only see *bunches* of wires, called *pipes*,
and they reshuffle their logical relations. For example, take the
switch rule
(A [B C])
s =|==|==|= .
[(A B) C]
Through pipes, logical inferences can go up and down, provided they
don't stumble one on another. For example, consider the following
derivations:
([a a] [ b b c]) ([a a] [ b b c])
s =| |====| |===|= wc_-|-|- | | |
[( | | | | ) |] | f | b |
| | | b | and | |wc_-|-|- | .
| |wc_-|-|- | | | | f |
| a | f | ( | | [ | | |])
wc_-|-|- | | | s =| |====| |===|=
[([a f] [b f]) c] [([a f] [b f]) c]
As you can see, the two wc_ rules can freely go up and down and pass
through the holes in the s rule. This example shows how wired
deduction deals with both type A and type B bureaucracy.
This also shows that employing this geometric criterion (sort of an
elastic deformation of graphs) avoids the problem of representing
non-canonical derivations: all derivations are canonical, and
convergence of the `rewriting system' is trivial.
So, what are derivations? Derivations are nets of the kind seen
above, whose general shape is
( <R> t ... t)
\|| | /
<net> .
/|| | \
[ <T> f ... f]
In other words, the premiss R is in the middle of any number of t
wires in conjunction and the conclusion T is in the middle of any
number of f wires in a disjunction. *No wires are created or
destroyed*: in this sense, this formalism is always *linear*. A
proof, of course, is a derivation with all t's in the premiss.
This setup clearly works for classical logic, and all our results
with CoS, and my preliminary work with subatomic proof theory, tell
us that this should work for *any* logic. Of course, in general f and
t are simply the units of whatever disjunction and conjunction one
has, for example they would be bottom and one for linear logic.
The general geometry is given by the wires: we *always* assume that
they live under a commutative and associative equivalence. In the
case of non-commutative logic, the non-commutativity will be
represented by the logical relation between wires, not by their
geometry. In other words: if you take the horizontal section of any
derivation like the ones above, you always have a relation web (back
to the origins).
So, this is propositional classical logic's system KSw; notice that
there are *no equations*:
(t t) [a a] (f t)
wi_ -|--|- , wc_ -|-|- , ww_ -|-|- ,
[a -a] [a f] [a f]
(A [B C]) [(A B) (C D)]
s =|==|==|= , m =|===X===|= .
[(A B) C] ([A C] [B D])
Of course, I have to show that this system is complete for classical
logic (soundness is trivial). I could do it semantically, for example
by showing how to get disjunctive normal forms and then realising
resolution and appeal to its completeness.
However, I also want to check that the complexity of proofs does not
grow wrt KS, which is the place where we mostly study it. So, in the
technicalities, you will find a complete proof of the admissibility
of KS equations for KSw.
What is the secret of success? Part of the reason is in the fact that
we can assume to have an unlimited supply of t's in conjunction and
f's in disjunction. These atoms can be brought wherever they are
needed by the switch rule. Doing this way does generate a small
amount of bureaucracy of the deductive-system kind, for contraction
and weakening rules. However, it is very easy to get rid of this
bureaucracy by simple permutations. This is not very geometrical, but
it is more geometrical than basically allowing [R f] = R and (R t) =
t everywhere, so I went that way. In any case, there always is
bureaucracy associated to the piling up of contraction and
weakenings, as I showed in the previous message to Frogs, and this
can be dealt with by using an appropriate deductive system with
non-local rules (or by using a straightforward equivalence on proofs).
If you have more or less clear what I tried to explain above, you can
jump directly to section 3 of the Technicalities and see KSw in
action while getting rid of KS equations.
TECHNICALITIES
==============
1 LANGUAGE
*Definition* We define the following:
- WW is a denumerable set of _wires_; we denote wires by natural numbers.
- PP is a set of _pipes_; we denote pipes by A, B, C, D and various
decorations.
- SSF is the language of _scheme skeleton formulae_, produced by
SSF ::= WW | PP | [SSF SSF] | (SSF SSF)
and such that no wire and no pipe appears twice in any element of SSF; we
denote scheme skeleton formulae by K; an _instance_ of a scheme skeleton
formula K is a scheme skeleton formula obtained by replacing in K any pipes
by scheme skeleton formulae.
*Example* K = [(1 2) A] is a scheme skeleton formula, while [(1 1) A] is not.
K' = [(1 2) (A B)] is an instance of K, while [(1 2) (A A)] is not.
[(1 2) ([3 4] (5 6))] is an instance of K'.
*Definition* AA is a denumerable set of _atoms_; we denote atoms by a, b and
c; on atoms we have an involution -: AA -> AA (i.e., --a = a); two special
atoms f and t, called _units_, belong to AA, and -f = t. A _scheme formula_ is
a couple (K, wr K -> AA), where wr K is the set of wires appearing in K; if no
pipes appear in K, then the scheme formula is a _formula_; formulae are denoted
by F.
*Example* If K = [(1 2) A] then (K, {1 -> a, 2 -> t}) is a scheme formula; if
K' = [(1 2) 3] then (K', {1 -> a, 2 -> t, 3 -> a}) is a formula, corresponding
to the classical propositional logic formula ((a ^ t) V a).
*Definition* The equivalence == on SSF is defined as the minimal equivalence
relation such that
[K K'] == [K' K] ,
(K K') == (K' K) ,
[K [K' K"]] == [[K K'] K"] ,
(K (K' K")) == ((K K') K") ,
if K == K' then [K K"] == [K' K"] and (K K") == (K' K") .
The equivalence == is applied naturally wherever scheme skeleton formulae
appear. _Structures_, denoted by P, Q, R, T, U and V, are formulae modulo ==.
*Examples and Notation* We usually omit indicating wires, and we write, for
example, [(a t) a] in the place of ([(1 2) 3], {1 -> a, 2 -> t, 3 -> a}). We
have that [(a b) [f a]] == [a [f (b a)]]. We drop unnecessary parentheses, so
[a [f (b a)]] can be written as [a f (b a)].
*Definition* Two structures R and T are _isomorphic_ if in their respective
==-equivalence classes there are two formulae which are equal modulo some
permutation of wires.
*Example* Let
R = ([([1 2] 3)]_==, {1 -> a, 2 -> b, 3 -> c}) ,
T = ([(4 [5 6])]_==, {4 -> c, 5 -> a, 6 -> b}) .
Clearly,
T = ([([5 6] 4)]_==, {5 -> a, 6 -> b, 4 -> c}) ;
we can consider the permutation {1 <-> 5, 2 <-> 6, 3 <-> 4}, and this shows
that R and T are isomorphic.
*Notation* We usually do not indicate pipes, rather we use structure
notation. So, for example, ([A B] C) is indicated as ([R T] U). This allows for
an important shortcut: when we repeat letters, like in (R R), we mean any
structure
([(K K')]_==, m), where m: wr (K + K') -> AA,
such that ([K]_==, m') and ([K']_==, m") are isomorphic, where m' and m" are
the restrictions of m to wr K and wr K', respectively.
*Example* ([R R] a) can be instantiated as ([(T T U) (T T U)] a) and
([(b f) (b f)] a), for example, but not as ([b c] a). ([R T] a) instead does
not impose any restriction on R and T.
*Definition* An _atomic inference rule_ is any expression of the kind
F
r ---,
F'
where F and F' are formulae such that the same wires appear in F and F'; r is
the _name_ of the rule. We adopt a notation such that wires are not explicitly
indicated, but they can be `followed', for example
((1 2), {1 -> f, 2 -> t})
ww_ -------------------------
([1 2], {1 -> a, 2 -> f})
is denoted by
(f t) (t f)
ww_ -|-|- or ww_ -X- .
[a f] [a f]
*Definition* A _local inference rule_ is any expression of the kind
K
r --- ,
K'
where K and K' are scheme skeleton formulae where no wires appear and such that
the same pipes appear in both; r is the _name_ of the inference. We adopt a
notation where we join vertically the pipes; for example
(A [B C])
s ---------
[(A B) C]
is denoted by
(A [B C]) (A [C B])
s =|==|==|= or s =|===X= .
[(A B) C] [(A B) C]
*Example* System KSw for classical propositional logic is defined by the
following rules
(t t) [a a] (f t)
wi_ -|--|- , wc_ -|-|- , ww_ -|-|- , for all a in AA,
[a -a] [a f] [a f]
(A [B C]) [(A B) (C D)]
s =|==|==|= , m =|===X===|= .
[(A B) C] ([A C] [B D])
The first three rule (schemes) are atomic, the last two are local. They are
called, respectively _wired interaction_, _wired contraction_, _wired
weakening_, _switch_ and _medial_.
2 COMPOSITION OF RULES
This part needs to be completed. For now, suffice to say that we compose rules
like in the calculus of structures. Of course, it is possible to define more
geometric notions of compositions, like for formalism B.
3 CLASSICAL PROPOSITIONAL LOGIC
*Proposition* The _contraction_ rule
[P P]
c_ ~|~^~ ,
P
is derivable for KSw.
*Proof* By structural induction on P. If P = a then consider
S[a a]
wc_ |-|--|-
|[a f]
s* =|=|==|= .
[S{a} f ]
If P = [R T] then consider
[R R T T]
c_ | |~|~^~
[R R | ]
c_ ~|~^~| .
[R T ]
If P = (R T) then consider
[(R T) (R T)]
m =|===X===|=
([| R] [T T])
c_ | | ~|~^~
([R R] | )
c_ ~|~^~ |
( R T )
<>
*Proposition* The following rules
f
aw_ ~|~ (_atomic weakening_),
a
[a a]
ac_ ~|~^~ (_atomic contraction_),
a
f (f f) R
r1 ~!^!~ , r2 ~|~^~ , r3 ~|~!~ ,
(f f) f (R t)
t [t t] [R f]
r5 ~|~!~ , r6 ~|~^~ , r8 ~|~^~
[t t] t R
are derivable for KSw.
*Proof* Consider, respectively:
(S{f} t)
s* =|=|==|=
|(f t)
ww_ |-|--|-
|[a f]
s* =|=|==|= ,
[S{a} f]
[a a]
c_ ~|~^~ ,
a
(S( f) t t t t )
s* =|========|==| | | |=
|( | | | t t )
wi_ | | | | -|-|-
|( | t t [t f] )
wi_ | | -|-|- | |
|( | [t f] [t |] )
2.s | | =|===X===|=
|( | [| t (f f)])
s | =/ /==|==| |=/ /=
|[(f f) (| [| | ])]
s* =|==| |===| | |=
[|( | |) (| [t t ]) ] S(f f)
wc_ | | | | -|--|- aw_ | | ~|~
[|( | |) (| [t f ]) ] |(f t)
s | | | =|==|==|= ww_ |-|--|-
[|( | |) (f t) | ] |[f f] (S{R} t)
ww_ | | | -|--|- | , s* =|=|==|= , s* =|=|==|= ,
[S( f f) f f f ] [S{f} f ] S(R t)
(S{ t} t t )
s* =|==|==| |=
|( t t t )
wi_ | -|--|- |
|([t f] | )
s | | | |
|[ | (f t)]
ww_ | | -|--|-
|[ | t f ] [t t] S[R f]
s* | =|==|==|= , c_ ~|~^~ , s* =|=|==|= .
[S[ t t] f ] t [S{R} f]
<>
*Theorem <PP>* In KSw, if S{P} is provable then S[P P] is provable.
*Proof* Induction on the length of the proof D of S{P}.
_Base Case_: If D = [(t t_t) f_f], we have to show that
[([(t n.t) (t n.t)] t_t) f_f] is provable, for n>= 0. Take
[( t t n.t n.t t_t) f_f]
wi_ -|--|- | | | |
[([ t f] | | | ) | ]
aw_ | ~|~ | | | |
[([ | t] n.t | | ) | ]
2.s =|====><=====|= | | .
[([(t n.t) (t n.t)] t_t) f_f]
_Inductive Cases_: If the bottommost rule instance in the proof of S{P} is like
in
__ __ __
|| || ||
S'{P} S{P'} S{P'}
r =|==|= or r |=|= or r |-|-
S{ P} S{P} S{P}
then use the induction hypothesis on
__ __
|| ||
__ S[P' P'] S[P' P']
|| r | | =|= r | | -|-
S'[P P] |[P' P ] |[P' P ]
r =|==| |= or r |=|= | or r |-|- | .
S[ P P] S[P P ] S[P P ]
Otherwise, the following cases are possible:
__
||
S'[Q (t t)]
1 S{ } = S'[a { }], P = [-a Q] and D = wi_ | | -|--|- : Consider
S'[Q a -a ]
__
||
S'[Q Q (t t) (t t)]
wi_ | | | | | -|--|-
| [| | (t t) a -a ]
wi_ | | | -|-|- | |
| [| | -a a a | ]
wc_ | | | |-|---|- |
| [| | | a f -a ]
s* =|==| | | | =X= ;
[S'[Q Q -a a -a] f ]
when Q is empty the argument is the same.
__
||
S'[Q a a]
2 S{ } = S'[{ } f], P = [Q a] and D = wc_ | |-|-|-: Consider
S'[Q a f]
__
||
S'[Q Q a a a a]
wc_ | | | |-|-|-|
| [| | | f a a]
c_ | | | | |~|~^~ ;
S'[Q Q a f a ]
when Q is empty the argument is the same.
__
||
S'[Q a a]
3 S{ } = S'[a { }], P = [f Q] and D = wc_ | |-|-|-: Consider
S'[Q a f]
__
||
S'[Q Q a a a a]
wc_ | | | | |-|-|-
| [| | a a a f]
wc_ | | |-|-|-| |
| [| | f a a |]
c_ | | | |~|~^~| ;
S'[Q Q f a f]
when Q is empty the argument is the same.
__
||
S'[Q (f t)]
4 S{ } = S'[{ } f], P = [Q a] and D = ww_ | | -|-|- : Consider
S'[Q a f ]
__
||
S'[Q Q (f t) (t f)]
ww_ | | | | | -|-|-
| [| | (f t) f a ]
ww_ | | | -|-|- | |
| [| | a f | | ]
c_ | | | |~|~~~^~| ;
S'[Q Q a f a ]
when Q is empty the argument is the same.
__
||
S'[Q (f t)]
5 S{ } = S'[a { }], P = [f Q] and D = ww_ | | -|-|- : Consider
S'[Q a f ]
__
||
S'[Q Q (t f) (f t)]
ww_ | | | | | -|-|-
| [| | (t f) a f ]
ww_ | | | -|-|- | |
| [| | f a a | ]
c_ | | | |~|~~~^~| ;
S'[Q Q f a f ]
when Q is empty the argument is the same.
__
||
S'[Q (R [T U U'])]
6 S{ } = S'[{ } U'], P = [(R T) U Q] and D = s | | =|==|==| |= :
Consider S'[Q (R T) U U' ]
__
||
S'[Q Q (R [T U U']) ([U' U T] R)]
s | | | | | | | =| |==|==|=
| [| | (| [| | | ]) | | (| |)]
s | | | =|==|==| |= | | | |
| [| | (| |) | U' U' | (| |)]
c_ | | | | | |~^~~~~~~|~ | | | ,
S'[Q Q (R T) U U' U (T R)]
when Q or U are empty the argument is the same.
__
||
S'[Q (R [T U U'])]
7 S{ } = S'[(R T) { } U'], P = [U Q] and D = s | | =|==|==| |= :
Consider S'[Q (R T) U U' ]
__
||
S'[Q Q (R [T U U']) ([U' U T] R)]
s | | | | | | | =| |==|==|=
| [| | (| [| | | ]) | | (| |)]
s | | | =|==|==| |= | | | |
| [| | (| |) | U' U' | (| |)]
c_ | | | | | |~^~~~~~~|~ | | |
S'[Q Q (R T) U U' U (T R)]
c_ | | | ~|~~|~.|........|..|.~^^^^~ ,
S'[Q Q (R T) U U' U ]
when Q or U are empty the argument is the same.
__
||
S'( R R' [(T T') U])
8 S{ } = S'[({ } R' T') U], P = (R T) and D = s | =| |====| |===|= :
Consider S'[(R R' T T') U]
__
||
S'[ ( R R' [(T T') U]) ( R R' [(T T') U])]
s | | | | | | =| >==< |=====|=
| [ ( R R' [(T T') |]) ( R T R' T') | ]
s | =| >==< |===|= | | | | |
| [ ( R T R' T') U ( | | | | ) U ]
c_ | | | | | ~^~....|..|....|..|....~|~
| [ ( | | R' T') ( R T | | ) | ]
m | =| |=====> >=======< <=====| |= |
| [([(| |) (R T)] [(R' T') (R' T')]) | ]
c_ | | | | | ~|~~|~~~~^^^^~ | ,
S'[([(R T) (R T)] R' T' ) U ]
when R or R' or T or T' are empty, but (R R'), (T T'), (R T) and (R' T') are
not empty, the argument is the same. The only case remaining to consider is
when (R' T') is empty, i.e., S{ } = S'[{ } U], P = (R T), but this
reduces to
case 6.
9 S{ } = S'([{ } R' U'] [T V]), P = [R U] and
__
||
S'[([R R' ] T) ([U U'] V)]
D = m | =| |===/ /===|===/ /====|= : Consider
S'( [R R' U U'] [T V])
__
||
S'[ ([R R'] T) ([R R'] T) ([U U'] V ) ([U U'] V) ]
m | =| |===/\/=/ /=\==|= | | | | | |
| [([ | | R R'] [T |]) ([| | ] V ) ([U U'] |) ]
m | | | | | | | =| |===/ X===/ /=\==|=
| [([ | | | | ] [T T]) ([ | | U U'] [V |])]
m | =| | | |=======\ \=====| | | |====\ \==| |=
| ([ | | | | | | | | ] [T T V V ])
c_ | | | | | | | | | ~|~^^^~|~
| ([ | R' | R' | U' | U'] [| | ])
c_ | |~|~.|~^~...............|~|~.|~^~ | | ,
S'([ R R' R U U' U ] [T V ])
when R or R' or U or U' are empty, but [R R'] and [U U'] are not empty, the
argument is the same.
<>
*Proposition <R7>* The rule
R
r7 ~|~!~
[R f]
is admissible for system KSw.
*Proof* Consider the topmost instance of r7 in a proof in KSw + {r7}:
__
||
[(S{R} m.t) f_f]
r7 ~|~!~ , for some m >= 0.
[ S[R f] f_f]
Let R = R'{a}, for some a; by Theorem <PP> there is a proof
__
||
[(S{R'[a a]} m.t ) f_f]
wc_ | | -|---|- | |
[(|{| [a f]} | ) | ]
s* =|=|==| |====|= |
[ |(| [| |] | ) | ]
s* |=|==|===|====|= |
[ |[| {|} (| m.t) ] | ]
| | | | ^ |
...
| | | | /| \ |
[ |[| {|} (| t t ) m-2.f] | ]
wi_ | | | | -|-|- | |
[ |[| {|} (| [t f]) m-2.f] | ]
s | | | =|==|==\===\=|= |
[ |[| {|} (f t ) m-1.f] | ]
ww_ | | | -|--|- | |
[ |[| {|} f f | ] | ]
s* =|=| | |==| |= | .
[ S[R'{a} f] f m-1.f f_f]
Proceed eliminating r7 instances one by one.
<>
*Proposition* The rule
(R t)
r4 ~|~^~
R
is admissible for KSw.
*Proof* Consider
S( R t)
r7 | ~|~~!~ |
|([R f] |)
s | =|==|==|=
|[ | (f t)]
ww_ | | -|--|-
|[ | f f ]
s* =|==|==| |= .
[ S{ R} f f ]
If S(R t) is provable in KSw, by Proposition <R7> then S{R} is also provable.
<>
*Theorem* System KSw is equivalent to system KS.
*Proof* All rules and equations of KS have admissible counterparts in KSw.
<>