Transcript Un Problema da 1 Milione di Dollari

Interpolation in \Lukasiewicz logic
and amalgamation of MV-algebras
Daniele Mundici
Dept. of Mathematics “Ulisse Dini”
University of Florence,
Florence, Italy
[email protected]
we all know what a simplex in Rn is
0-simplex
1-simplex
2-simplex
3-simplex
polyhedron P= finite union of simplexes Si in Rn
P need not be convex, nor connected
a polyhedron P = USi is said to be rational
if so are the vertices of every simplex Si
our main themes:
rational polyhedra and
\Lukasiewicz logic
Chapter 1: Local Deduction
as a main ingredient
of interpolation and amalgamation
\Lukasiewicz logic L∞
•
•
FORMULAS are exactly the same as in boolean logic
•
•
•
V(¬F) = 1–V(F)
•
CONSEQUENCE RELATION: F |– G means that
every valuation satisfying F also satisfies G
any VALUATION V evaluates formulas into the real
unit interval [0,1] via the inductive rules:
V(F —> G) = min(1, 1–V(F)+V(G))
Therefore, every valuation V is uniquely determined by
its values on the variables: V(X1),...,V(Xn)
formulas yield functions f:[0,1]n—>[0,1]
as boolean formulas yield f:{0,1}n—>{0,1}
• every formula F(X1,...,Xn) determines
a map fF : [0,1]n —>[0,1] by
• fXi = the ith coordinate map
• f¬F = 1 – fF
• fF —> G = min(1, 1 – fF + fG)
definable functions of one variable
for each formula F, its
associated function fF is
continuous, linear, and each
linear piece has integer
coefficients (for short, fF is a
McNaughton function)
the ONESET fF-1(1) of fF
is the set of valuations
satisfying the formula F
oneset(fF)=zeroset(¬fF)
oneset of fF = Mod(F)
•
by induction on the
number of connectives
in F, the oneset of fF
is a rational polyhedron,
and so is the oneset of
f¬F and of fF —> G
EACH ZEROSET AND EACH
ONESET IS A RATIONAL
POLYHEDRON IN [0,1]n
(Local) Deduction Theorem
Theorem. For any two formulas A and B, the following
conditions are equivalent:
1. Every valuation satisfying A also satisfies B
2. For some m=1,2,... the formula
A—>(A—>(A—>...—>(A—>(A—>B))...)) is a tautology
3. B is obtained from A and the tautologies via Modus Ponens
PROOF.
2—>3 easy; 3—>1 induction; 1—>2 is proved geometrically
assume oneset(fA) contained in oneset(fB)
1
let T be a triangulation
of [0,1] such that the
functions fA and fB
both formulas A and B
are linear over each
interval of T
fB
fA
1
fA & fA < fA
1
applying \Lukasiewicz
conjunction to A,
from the formula
A&A we get obtain a
minorant fA&A of fA,
still with the same
one set of fA
fB
fA&A
Recall definition
P&Q = ¬(P —> ¬Q)
1
fA & fA & fA < fA & fA < fA
1
by iterated application
of the \Lukasiewicz
conjunction we obtain a
function
fkA= fA&fA&...&fA
with the same oneset of
fA, and with the
additional property
that fAk ≤ fB
fB
f kA
1
for large k this will hold at every simplex of T
1
fB
in other words, we have
the tautology Ak—>B,
which is the same as
the desired tautology
fA
1
A—>(A—>(A—>...—>(A—>(A—>B))...))
Chapter 2: Interpolation
(as a main tool to amalgamation)
interpolation/amalgamation
•
Craig interpolation theorem fails in \Lukasiewicz logic,
because the tautology x¬x—>y¬y has no interpolant
•
deductive interpolation is like Craig interpolation, with the |–
symbol in place of the implication connective (more soon)
•
over the last 25 years, several proofs have been given of
deductive interpolation for \Lukasiewicz infinite-valued
propositional logic
•
deductive interpolation, together with local deduction, is a main
tool to prove the amalgamation theorem for the algebras of
\Lukasiewicz infinite-valued logic
amalgamation: many proofs
•
the first proof of amalgamation used the categorical
equivalence between MV-algebras and unital lattice-ordered
groups (relying on Pierce's amalgamation theorem).
•
in the early eighties I heard from Andrzej Wro\’nski during one
of his visits to Florence, that the Krakow group had a proof of
the amalgamation property for MV-algebras without negation
(i.e., Komori’s C algebras)
•
recent proofs, like the proof by Kihara and Ono, follow by
applying to MV-algebras results in universal algebra
•
I will present a simple geometric proof of the amalgamation
theorem, using Deductive Interpolation
background literature
F. Montagna, Interpolation and Beth's property in propositional manyvalued logics: A semantic investigation, Annals of Pure and Applied
Logic, 141: 148-179, 2006. This is based on:
N.Galatos, H. Ono, Algebraization, parametrized local deduction
theorem and interpolation for substructural logics over FL, Studia
Logica, 83:279-308, 2006. For the proof of Theorem 5.8, the
following is needed:
A. Wro\'nski, On a form of equational interpolation property, In:
Foundations of Logic and Linguistic, G.Dorn, P. Weingartner, (Eds.),
Salzburg, June 19, 1984, Plenum, NY, 1985, 23-29. For the proof of
Theorem I on page 25, the following is needed:
P.D. Bacisch, Amalgamation properties and interpolation theorems for
equational theories, Algebra Universalis, 5:45-55, 1975.
(Deductive) Interpolation
If F |– G then there is a formula J such that F |– J,
J |– G, and each variable of J is a variable of both
F and G
our proof will be entirely geometrical
rational polyhedra are preserved under projection
the projection
of a (rational) polyhedron
onto a (rational) hyperplane
is a (rational) polyhedron
we record this fact as the PROJECTION LEMMA
rational polyhedra are preserved under
perpendicular cylindrification
we record this fact as the CYLINDRIFICATION LEMMA
oneset of fF = Mod(F)
recall: THE ZEROSET (AND
THE ONESET) OF ANY
\LUKASIEWICZ FORMULA IS
A RATIONAL POLYHEDRON
IN [0,1]n
we now prove the converse:
EACH RATIONAL POLYHEDRON IN [0,1]n IS THE
ZEROSET OF SOME \LUKASIEWICZ FORMULA
rational half-spaces in
a rational line L in [0,1]2
mx+ny+p=0, with m,n,p integers, m>0
H
n
[0,1]
PROBLEM:
Does there exist
a formula F such
that the zeroset
of fF coincides
with H ?
ANSWER:
Yes, by induction
on |m|+|n|
H is one of the half-planes bounded by L in the square [0,1]2
then every rational polyhedron is a zeroset
this blue half-space is a zeroset
and this rational polyhedron
(formulas can express unions)
then so is this rational triangle
(formulas can express intersections)
ANY RATIONAL
POLYHEDRON IN [0,1]n
IS THE ZEROSET OF
SOME fF
this was known to McNaughton (1951)
FOLKLORE LEMMA
Rational polyhedra contained in the n-cube [0,1]n
coincide with zerosets (and also coincide with onesets)
of definable maps, i.e., functions of the form fF
where F ranges over formulas in n variables
we record the FOLKLORE LEMMA by writing:
RATIONAL POLYHEDRA=ONESETS=MODELSETS
Deductive interpolation
TH E OR E M If F
th at
F
|Ğ J,
|Ğ G then th ere is a fo rm ul a J such
J |Ğ G , a nd va r(J ) = var (F ) v ar (G)
PROOF. We may write var(F) = X u Z
var(G) = Y u Z,
for X,Y,Z pairwise disjoint sets of variables
Mod(F) = fF-1(1) = P, which by the Folklore Lemma is a
rational polyhedron in [0,1]XuZ
by the Projection Lemma, the projection of P onto RZ is
a rational polyhedron Q contained in [0,1]Z
Mod(G) = fG-1(1) = R, a rational polyhedron in [0,1]YuZ
Z
Mod(G)=R
Q
Mod(F) = P
Y
X
the hypothesis F |— G states that, in the space RXuYuZ
Mod(F) is contained in Mod(G)
regarding J as a formula in the variables
X,Z, then Mod(J) is this blue rectangle!
by the Folklore
Lemma, there
is a formula
J(Z) such that
Q=Mod(J)
Z
Q = Mod(J)
Mod(F) = P
Y
X
We then obtain the first half of interpolation: F |— J
regarding J as a formula in Y,Z, then Mod(J) is this blue rectangle!
Z
Q=Mod(J)
Mod(F) = P
Mod(G)=R
Y
X
in the space RYuZ , Mod(J) is contained in Mod(G)
We then obtain the second half of interpolation: J |— G
Chapter 3: Amalgamation
of the algebras of \Lukasiewicz logic,
i.e., Chang MV-algebras
MV-algebras (in Wajsberg’s version)
directly from \Lukasiewicz axioms
A—>(B—>A)
(A—>B)—>((B—>C)—>(A—>C))
((A—>B)—>B)—> ((B—>A)—>A)
(¬A—>¬B)—>(B—>A)
the amalgamation property
Z
A
we have
B
the usual setup
Z
A
we have
B
we want
D
henceforth, all blue maps are one-one
the embedding of Z into A
Z
let us focus attention
on the embedding of
Z into A
A
without loss of generality , Z is a subalgebra of A
thus the set A is the disjoint union of Z and some set X, A=Z U X
extending maps to homomorphisms
FREEZ
sZ
the identity map z—>z uniquely
extends to a homomorphism sZ of
the free MV-algebra FREEZ onto Z
Z
similarly, the identity map a—> a uniquely extends to
a homomorphism sA of FREEA onto A
let
ker sZ and ker sA denote the kernels of these maps
ker(sZ)
all blue arrows are inclusions
all red arrows are surjections
FREEZ
ker(sA)
sZ
Z
FREEXUZ
sA
A
LEM M A
ke r( s Z ) = ke r( s A )  F R EE Z
intuitively, this trivial Largeness Lemma states that
ker(sZ) is as large as possible in ker(sA).
Z
A
B
ker(sZ)
ker(sA)
FREEZ
ker(sB)
sz
FREEXUZ
sA
A
Z
FREEYUZ
sA
B
ker(sZ)
ker(sA)
FREEZ
ker(sB)
sz
FREEXUZ
sA
Z
A
FREEYUZ
sA
B
FREEXUYUZ
I = the ideal generated by ker(sA) U ker(sB)
ker(sZ)
ker(sA)
FREEZ
ker(sB)
sz
FREEXUZ
sA
Z
A
FREEYUZ
sA
B
D
FREEXUYUZ
I = the ideal generated by ker(sA) U ker(sB)
ker(sZ)
ker(sA)
FREEZ
ker(sB)
sz
FREEXUZ
Z
sA
A
µ(x/ ker(sA)) = x/i
there remains to be
proved that µ is
one-one
FREEYUZ
sA
B
µ
D
FREEXUYUZ
i = the ideal generated by ker(sA) U ker(sB)
Let e be an element
of FREEXUYUZ
such that e/i =0.
We must prove
e/ker(sA) = 0
e/i = 0 means that e is an element of i. In other words, (theories ~
ideals) a, b |– e for some a in ker(sA) and b in ker(sB)
end of the proof of amalgamation
Chapter 4:
Further geometric
developments on projective MValgebras
why should we insist in giving many proofs of
MV-amalgamation and interpolation?
•
because MV-algebras provide a benchmark for other
structures of interest in algebraic logic
•
because interpolation and amalgamation are deeply related to
many fundamental logical-algebraic-geometric notions:
•
quantifier elimination, cut elimination, joint consistency,
joint embedding, unification, projectives,...
•
let us briefly review what is known about finitely generated
projective MV-algebras, i.e., retracts of FREEn for some n
•
this is joint work with Leonardo Cabrer, to appear in
Communications in Contemporary Math., and based on
earlier joint work on Algebra Universalis 62 (2009) 63–74.
projectives are routinely characterized by duality
•
Every n-generated projective MV-algebra A is finitely
presented (essentially, Baker)
•
A is finitely presented iff A=M(P) for some polyhedron
P lying in some n-cube [0,1]n (Baker-Beynon duality)
•
DEFINITION P is said to be a Z-retract if the MValgebra M(P) is projective
•
Problem: characterize Z-retracts, among all polyhedra
a first property of Z-retracts:
they are retracts of some cube [0,1]n
this property is not easy to handle;
thus, we must find equivalent conditions
for a polyhedron P to be retract of [0,1]n
to check if P is a retract it suffices to check
that all homotopy groups of P are trivial
The elements of the
fundamental group π1(P)
(introduced by Poincaré) of a
connected polyhedron P are
the equivalence classes of the
set of all paths with initial and
final points at a given
basepoint p, under the
equivalence relation of
homotopy. The fundamental
groups of homeomorphic
spaces are isomorphic.
equivalents for P to be a retract of [0,1]n
THEOREM. For any polyhedron P in [0,1]n the following
conditions are equivalent:
(a) P is a retract of [0,1]n
(b) P is connected and all homotopy groups πi(P) are trivial
(c) P is contractible (can be continuously shrunk to a point).
Proof. (a)—>(b) by the functorial properties of the
homotopy groups πi . The implications (b)—>(a) and (b)—
>(c) follow from Whitehead theorem in algebraic topology.
(c)—>(b) is trivial. QED
let P be this polyhedron
P is not a Zretract, because
it is not simply
connected
M(P) is not
projective
a second property of Z-retracts:
P must contain a vertex of [0,1]n
P is not a Z-retract,
because it does not
contain any vertex of
the unit square
M(P) is not
projective
a third property: strong regularity
PROPOSITION If P is a Z-retract, then P has a
triangulation Ω such that the affine hull of every maximal
simplex in Ω contains some integer point of Rn
1
0
1
this P is not a Zretract: for, the affine
hull of the vertical red
segment does not
contain any integer
point
M(P) is not
projective
projectiveness: 3 necessary conditions
THEOREM (L.Cabrer, D.M., 2009) If A is a finitely generated
projective MV-algebra, then up to isomorphism, A=M(P) for
some rational polyhedron lying in [0,1]n such that
(i) P contains some vertex of [0,1]n,
(ii) P is contractible, and
(iii) P is strongly regular.
are these three conditions also sufficient for
an MV-algebra A to be finitely generated projective ?
yes, when the maximal spectrum is onedimensional
THEOREM (L.Cabrer, D.M.) Suppose the maximal
spectrum of A is one-dimensional. Then A is ngenerated projective if and only if A is isomorphic to
M(P) for some contractible strongly regular rational
polyhedron in [0,1]n containing a vertex of [0,1]n.
It is not known if these three conditions are sufficient
in general.
They become sufficient if contractibility is strengthened to
collapsibility
a sequence of collapses
a sequence of collapses
a sequence of collapses
a sequence of collapses
a sequence of collapses
a sequence of collapses
a sequence of collapses
a sequence of collapses
a sufficient condition for P to be a Z-retract,
i.e., for M(P) to be projective
THEOREM (L.Cabrer, D.M., Communications in
Contemporary Mathematics)
If P has a collapsible strongly regular triangulation
containing a vertex of [0,1]n then M(P) is projective.
algebra
geometry
A is finitely presented
homomorphism
isomorphism
indecomposable
A is free n-generated
A is n-generated
dim(maxspec(A))=d
A=M(P) is projective
A=M(P), P a polyhedron
Z-map
Z-homeomorphism
P is connected
P=unit cube [0,1]n
P lies in [0,1]n
dim(P)=d
P is a Z-retract
\Lukasiewicz logic and MV-algebras together
are a rich source of geometric inspiration
thank you