Is the principle of contradiction a consequence of 𝑥𝑥 = 𝑥 ?
jean-yves beziau
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
JAIME ALEJANDRO BOHORQUEZ VILLAMIZAR
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
----------------------------
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
Ingeniería de Sistemas
Escuela Colombiana de Ingeniería
AK 45 # 205 - 59, Bogotá, Colombia
Enviado: martes, 19 de julio de 2016 10:03 a. m.
Para: logi...@dimap.ufrn.br
Asunto: [Logica-l] Is the principle of contradiction a consequence of 𝑥𝑥 = 𝑥 ?
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 logica-l+u...@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
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.