Dear Jean-Yves
As they say, perception is intentional. I have some remarks about certain
points I liked and found interesting in your paper.
0) This "lining-device" (you talk about): a series of statements written in
separate lines vertically connected to express a derivation, seems to me, is a
basic and straight-forward way with which the lay mathematician (George Boole
being one of them) expresses mathematical arguments and calculations.
1) In relation with table 3, we could go beyond the interpretation of CPL as a
Boolean algebra on (0,1) and applying it, as well, to predicate logic.
Universal and existential quantifications would be, respectively (and
intuitively) interpreted as iterated conjunctions and disjunctions ranging over
all possible values that the corresponding bound variables can take.
2) Adding to what is said in (1), we could connect the lines of the
"lining-device" (as you did In table 7) with a bidirectional inference
relation, that you appropriately, named logical equivalence. As this logical
equivalence is actually a congruence, we end up calculating on a Lindenbaum
algebra. So, we can prove in first order logic by calculating in the associated
Lindenbaum algebra.
3) The main inference rule appropriate to prove in a formal system as suggested
in (2) would be based on a controlled form of rewriting (called textual
substitution) that replaces (all occurrences of) a subformula in one of the
premises by a logically equivalent one ("substitution of equals for equals"
or, maybe better, "substitution of equivalents for equivalents") according to
the second premise that expresses such equivalence. Such inference rule is
called Leibniz rule and goes as follows
E[z / P] P == Q
----------------------------
E[z / Q]
This means that E[z / Q] is obtained by replacing every mention of P in E[z /
P] by Q, its equivalent according to premise P == Q.
In the same way that Modus Ponens privileges the use of the implication
connective over all the others, Leibniz rule gives preference to the use of
logical equivalence ('==" as used above) as boolean connective.
4) Now, lines in the "lining-device" are not only connected by intermediate
'-||-' symbols (using your notation), but also, these bi-inferential symbols
are accompanied by the equivalence (the second premise in the Leibniz rule)
justifying the inferential step.
This way, the "lining-device" evolves into a linear 'proof format' compatible
with the way mathematicians proceed. By an "abus de langage", the symbol -||-
is replaced by the symbol used for the boolean connective for equivalence (==,
as I used in this text, or the more common <=>, although this one suggests a
bi-implication rather than an equivalence).
The end result of this, is a formal system for first order logic currently
known as calculational logic. The calcultional proof format was originally
introduced by Dijkstra and Scholten [0] based on ideas due to W.H.J. Feijen.
Due to the particular way Dijkstra and Scholten presented this contribution (in
a rigorous, but informal way, where they did not distinguish between formulas
and inference rules), it was not appreciated by logicians. However, V.
Lifschitz in [1] gave a formal counterpart of Dijkstra-Scholten calculational
proofs. Recently, C. Rocha [2] explained the proof-theoretic foundations of
Dijkstra-Scholten logic as a formal system in terms of rewriting theory.
Calculational logic can be viewed as an interesting discovery in logic, in the
same way that natural deduction was, when it was first introduced by Gentzen.
Notwithstanding this, it has so far been largely unnoticed. This is a pity,
since, as you pointed out, there seems to be strong ties between notations and
conceptual frameworks, and so, the resulting proof-theoretical concepts and
proof-checking methods coming out from calculational logic could be very
different from those coming out from natural deduction and its related formal
systems.
[0] E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program
Semantics. Springer Verlag, 1990.
[1] Vladimir Lifschitz. On calculational proofs. Ann. Pure Appl.
Logic,113(1-3):207–224, 2001.
[2] Camilo Rocha. The formal system of Dijkstra and Scholten. In Narciso
Martı́-Oliet, Peter Csaba Ölveczky, and Carolyn L. Talcott, editors, Logic,
Rewriting, and Concurrency,
volume 9200 of Lecture Notes in Computer Science, pages 580–597. Springer, 2015.
Well, this is all your paper made me think about, and this is why I liked it.
Note: there quite a few typos you have to correct.
Greetings
Jaime A Bohórquez
Ingeniería de Sistemas
Escuela Colombiana de Ingeniería
AK 45 # 205 - 59, Bogotá, Colombia
________________________________
De: jean-yves beziau <[email protected]>
Enviado: martes, 19 de julio de 2016 10:03 a. m.
Para: [email protected]
Asunto: [Logica-l] Is the principle of contradiction a consequence of 𝑥𝑥 = 𝑥 ?
Dear Colleagues
You will find through the link below a first draft of my paper
Is the principle of contradiction a consequence of 𝑥𝑥 = 𝑥 ?
http://www.jyb-logic.org/papers/jyb-boole.pdf
This corresponds to a lecture about PROPOSITION IV of Chapter III of the Laws
of Thought of Boole I presented at THE 12TH INTERNATIONAL CONFERENCE “LOGIC
TODAY: DEVELOPMENTS AND PERSPECTIVES”
June 22–24, 2016, St. Petersburg, Russia
http://ocs.philosophy.spbu.ru/index.php/logic12/index/pages/view/program
Comments are welcome.
Best Wishes
Jean-Yves
--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos
do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um
e-mail para
[email protected]<mailto:[email protected]>.
Para postar nesse grupo, envie um e-mail para
[email protected]<mailto:[email protected]>.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLA9Q5VSQcw8cDynThGEqhyqTVn5TnyxTzf9973RKTC7Eg%40mail.gmail.com<https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLA9Q5VSQcw8cDynThGEqhyqTVn5TnyxTzf9973RKTC7Eg%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um
e-mail para [email protected].
Para postar neste grupo, envie um e-mail para [email protected].
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/BY2PR0101MB0886E7352B8BF8C4F75B9B1DAD080%40BY2PR0101MB0886.prod.exchangelabs.com.
