Iranian Association of Logic
Owner
Iranian Association of Logic (IAL) is the owner of Logical Letter.
About Logical Letter
Logical Letter is the English-language newsletter of the Iranian Association for Logic (IAL). It brings news and ideas from Iran’s logic community to readers at home and abroad, and gives that community a shared place to report on its work, its meetings and its questions.
Logic in Iran draws on several traditions at once. There is the long history of Avicennan and post-Avicennan logic, and there is active research in mathematical logic, philosophical logic and the foundations of computer science. Logical Letter is meant to reflect that range. Each issue may include short research articles and expository essays, reports from the Association’s annual conferences and World Logic Day events, interviews with logicians, book reviews, and news about seminars, theses and opportunities for students and researchers.
The newsletter is written for working logicians, but not only for them. We hope it will also be useful to students taking their first steps in the field, to mathematicians, philosophers and computer scientists who use logic in their own work, and to anyone curious about what logic is and why it matters.
Contributions are welcome in all areas of logic, including mathematical and philosophical logic, the philosophy of logic and mathematics, traditional and historical logic, logic and computation, and logic education. Proposals, articles and news items can be sent to logicalletter@ialogic.ir.
Logical Letter is published quarterly by the Iranian Association for Logic.
0 days
Average Time to First Review
73 days
Average Time to Accept
0 days
Average Time to Publish
100 %
Acceptance Rate
Editor-in-chief
Ali Valizadeh, PhD
Assistant Professor, Department of Mathematics and Statistics, University of Isfahan, Isfahan, Iran
Scientific Supporters
Iranian Association for Logic
Articles
Avicenna's Modal Syllogistic: A Persian Contribution to the History of Logic
H. Mohammad Ghorbanian
Aims This article introduces the modal syllogistic of Avicenna (Ibn Sīnā, d. 1037) to readers trained in modern logic and explains why it remains one of the most original episodes in the history of the subject.
Approach The discussion is expository and historical. It sets out the problem Avicenna inherited from Aristotle's Prior Analytics, reconstructs the main features of his analysis of categorical and modal propositions, and follows the reception of his ideas in later logic written in Arabic and Persian.
Main Points Avicenna's central move was to make the truth conditions of propositions explicit, in particular the temporal conditions under which a predicate belongs to a subject. His distinction between the substantial and the descriptive readings of a proposition, together with his broad reading of the subject term, explains the asymmetries of Aristotle's modal syllogisms that had puzzled earlier commentators. The same attention to truth conditions shaped his theory of quantified conditional propositions.
Conclusion Avicenna's logic is not a museum piece. It shows how careful semantic analysis can decide questions of validity, it shaped centuries of teaching in Iran and beyond, and it continues to repay formal study.
View Abstract
Approach The discussion is expository and historical. It sets out the problem Avicenna inherited from Aristotle's Prior Analytics, reconstructs the main features of his analysis of categorical and modal propositions, and follows the reception of his ideas in later logic written in Arabic and Persian.
Main Points Avicenna's central move was to make the truth conditions of propositions explicit, in particular the temporal conditions under which a predicate belongs to a subject. His distinction between the substantial and the descriptive readings of a proposition, together with his broad reading of the subject term, explains the asymmetries of Aristotle's modal syllogisms that had puzzled earlier commentators. The same attention to truth conditions shaped his theory of quantified conditional propositions.
Conclusion Avicenna's logic is not a museum piece. It shows how careful semantic analysis can decide questions of validity, it shaped centuries of teaching in Iran and beyond, and it continues to repay formal study.
Gödel's Incompleteness Theorems: What They Do and Do Not Show
N. Roshandel Tavana
Aims This article gives a precise but accessible account of Gödel's two incompleteness theorems and separates what they establish from the many claims that are made in their name.
Approach The theorems are stated carefully for effectively axiomatized theories of arithmetic. The main steps of the proof (arithmetization, representability and the diagonal lemma) are explained informally, and the later strengthenings due to Rosser, Hilbert, Bernays and Löb are described.
Main Points The first theorem shows that no consistent, effectively axiomatized theory that contains a modest amount of arithmetic can decide every arithmetical sentence. The second shows that such a theory cannot prove its own consistency. Both results depend essentially on their hypotheses. They do not imply that every formal system is incomplete, that mathematical truth is unknowable, that we cannot be confident of the consistency of arithmetic, or that the human mind cannot be a machine.
Conclusion The incompleteness theorems are precise statements about formal theories. Read correctly, they mark a lasting limit on the axiomatic method and open several of the most fruitful directions in modern logic.
View Abstract
Approach The theorems are stated carefully for effectively axiomatized theories of arithmetic. The main steps of the proof (arithmetization, representability and the diagonal lemma) are explained informally, and the later strengthenings due to Rosser, Hilbert, Bernays and Löb are described.
Main Points The first theorem shows that no consistent, effectively axiomatized theory that contains a modest amount of arithmetic can decide every arithmetical sentence. The second shows that such a theory cannot prove its own consistency. Both results depend essentially on their hypotheses. They do not imply that every formal system is incomplete, that mathematical truth is unknowable, that we cannot be confident of the consistency of arithmetic, or that the human mind cannot be a machine.
Conclusion The incompleteness theorems are precise statements about formal theories. Read correctly, they mark a lasting limit on the axiomatic method and open several of the most fruitful directions in modern logic.
Intuitionistic Logic and the Meaning of Proof
A. Valizadeh
Aims This article introduces intuitionistic logic as a philosophical position about the nature of mathematics and as a precise logical system, and explains why it remains central to the philosophy of mathematics and to computer science.
Approach The discussion follows the development of the subject from Brouwer's critique of classical reasoning, through Heyting's formalization and the proof interpretation of Brouwer, Heyting and Kolmogorov, to Kripke's semantics and Dummett's meaning-theoretic arguments.
Main Points Intuitionistic logic arises when the meaning of a mathematical statement is explained by what counts as a proof of it rather than by truth conditions that may transcend our knowledge. On this view the law of excluded middle is not a logical law, while most of ordinary reasoning remains valid. Classical and intuitionistic logic are closely related by translations, and intuitionistic logic has natural semantics in terms of growing states of knowledge.
Conclusion Intuitionism is not only a historical episode in the foundations of mathematics. Its central idea, that meaning is given by proof, remains a live option in the philosophy of language and underlies modern constructive mathematics and type theory.
View Abstract
Approach The discussion follows the development of the subject from Brouwer's critique of classical reasoning, through Heyting's formalization and the proof interpretation of Brouwer, Heyting and Kolmogorov, to Kripke's semantics and Dummett's meaning-theoretic arguments.
Main Points Intuitionistic logic arises when the meaning of a mathematical statement is explained by what counts as a proof of it rather than by truth conditions that may transcend our knowledge. On this view the law of excluded middle is not a logical law, while most of ordinary reasoning remains valid. Classical and intuitionistic logic are closely related by translations, and intuitionistic logic has natural semantics in terms of growing states of knowledge.
Conclusion Intuitionism is not only a historical episode in the foundations of mathematics. Its central idea, that meaning is given by proof, remains a live option in the philosophy of language and underlies modern constructive mathematics and type theory.
Logic Meets Computation: From the Curry--Howard Correspondence to Proof Assistants
A. Mirsanei
Aims This article explains the correspondence between proofs and programs known as the Curry--Howard correspondence, and shows how it has led to proof assistants that are now used to verify both mathematics and software.
Approach Starting from natural deduction and the simply typed lambda calculus, the article sets out the correspondence between propositions and types, proofs and programs, and proof normalization and evaluation, follows its main extensions, and reviews the leading proof assistants and their applications.
Main Points The correspondence is not an analogy but a precise structural identity: a proof in intuitionistic natural deduction is a typed program, and simplifying the proof is running the program. Dependent types extend the correspondence to quantifiers and allow mathematical statements and their proofs to be written and checked in a single language.
Conclusion The correspondence has turned an abstract result of logic into a practical technology that has verified major theorems and critical software.
View Abstract
Approach Starting from natural deduction and the simply typed lambda calculus, the article sets out the correspondence between propositions and types, proofs and programs, and proof normalization and evaluation, follows its main extensions, and reviews the leading proof assistants and their applications.
Main Points The correspondence is not an analogy but a precise structural identity: a proof in intuitionistic natural deduction is a typed program, and simplifying the proof is running the program. Dependent types extend the correspondence to quantifiers and allow mathematical statements and their proofs to be written and checked in a single language.
Conclusion The correspondence has turned an abstract result of logic into a practical technology that has verified major theorems and critical software.
Paradoxes of Truth: The Liar and Its Modern Solutions
H. Bastin
Aims This article surveys the Liar paradox and the main families of solutions proposed since the 1930s, and assesses what each solution costs.
Approach After a brief history of the paradox, including its treatment by logicians in Shiraz in the fifteenth century, the article presents Tarski's undefinability theorem and hierarchy of languages, Kripke's fixed-point theory of truth, contextualist and revision-theoretic approaches, and paraconsistent and paracomplete logics. The problem of ``revenge'' paradoxes is used as a common test.
Main Points The Liar shows that three natural assumptions cannot all be kept: that a language can talk about the truth of its own sentences, that truth obeys the equivalence ``? is true if and only if ?'', and that classical logic holds without restriction. Each solution gives up one of these assumptions or restricts it. Every solution so far proposed faces some form of revenge.
Conclusion There is no consensus solution to the Liar. The paradox remains a productive test for theories of truth, meaning and logical consequence, and its study has led to some of the most important technical work in philosophical logic.
View Abstract
Approach After a brief history of the paradox, including its treatment by logicians in Shiraz in the fifteenth century, the article presents Tarski's undefinability theorem and hierarchy of languages, Kripke's fixed-point theory of truth, contextualist and revision-theoretic approaches, and paraconsistent and paracomplete logics. The problem of ``revenge'' paradoxes is used as a common test.
Main Points The Liar shows that three natural assumptions cannot all be kept: that a language can talk about the truth of its own sentences, that truth obeys the equivalence ``? is true if and only if ?'', and that classical logic holds without restriction. Each solution gives up one of these assumptions or restricts it. Every solution so far proposed faces some form of revenge.
Conclusion There is no consensus solution to the Liar. The paradox remains a productive test for theories of truth, meaning and logical consequence, and its study has led to some of the most important technical work in philosophical logic.
Why Teach Logic? Reflections on Logic Education in Schools and Universities
F. Ranjbari
Aims This article asks what logic education is for, what research says about its effects, and how logic teaching in schools and universities, particularly in Iran, might be improved.
Approach The article reviews three common justifications for teaching logic, examines evidence from the psychology of reasoning and from mathematics education on what students learn from logic courses, and considers the current place of logic in Iranian curricula. It ends with practical proposals.
Main Points Logic is commonly taught in order to improve reasoning in general, to support the study of mathematics and computer science, and as part of a liberal and philosophical education. Research shows that formal logic courses do not automatically improve everyday reasoning, but that well-designed teaching that connects formal rules with meaningful contexts can have real effects. Students' difficulties with implication and quantifiers are a major obstacle in learning mathematical proof.
Conclusion Logic deserves a secure place in education, but its value depends on how it is taught. Integrating traditional and modern logic, teaching for transfer, using software tools and investing in teacher preparation are the main priorities.
View Abstract
Approach The article reviews three common justifications for teaching logic, examines evidence from the psychology of reasoning and from mathematics education on what students learn from logic courses, and considers the current place of logic in Iranian curricula. It ends with practical proposals.
Main Points Logic is commonly taught in order to improve reasoning in general, to support the study of mathematics and computer science, and as part of a liberal and philosophical education. Research shows that formal logic courses do not automatically improve everyday reasoning, but that well-designed teaching that connects formal rules with meaningful contexts can have real effects. Students' difficulties with implication and quantifiers are a major obstacle in learning mathematical proof.
Conclusion Logic deserves a secure place in education, but its value depends on how it is taught. Integrating traditional and modern logic, teaching for transfer, using software tools and investing in teacher preparation are the main priorities.
Paradoxes of Truth: The Liar and Its Modern Solutions
H. Bastin
Aims This article surveys the Liar paradox and the main families of solutions proposed since the 1930s, and assesses what each solution costs.
Approach After a brief history of the paradox, including its treatment by logicians in Shiraz in the fifteenth century, the article presents Tarski's undefinability theorem and hierarchy of languages, Kripke's fixed-point theory of truth, contextualist and revision-theoretic approaches, and paraconsistent and paracomplete logics. The problem of ``revenge'' paradoxes is used as a common test.
Main Points The Liar shows that three natural assumptions cannot all be kept: that a language can talk about the truth of its own sentences, that truth obeys the equivalence ``? is true if and only if ?'', and that classical logic holds without restriction. Each solution gives up one of these assumptions or restricts it. Every solution so far proposed faces some form of revenge.
Conclusion There is no consensus solution to the Liar. The paradox remains a productive test for theories of truth, meaning and logical consequence, and its study has led to some of the most important technical work in philosophical logic.
View Abstract
Approach After a brief history of the paradox, including its treatment by logicians in Shiraz in the fifteenth century, the article presents Tarski's undefinability theorem and hierarchy of languages, Kripke's fixed-point theory of truth, contextualist and revision-theoretic approaches, and paraconsistent and paracomplete logics. The problem of ``revenge'' paradoxes is used as a common test.
Main Points The Liar shows that three natural assumptions cannot all be kept: that a language can talk about the truth of its own sentences, that truth obeys the equivalence ``? is true if and only if ?'', and that classical logic holds without restriction. Each solution gives up one of these assumptions or restricts it. Every solution so far proposed faces some form of revenge.
Conclusion There is no consensus solution to the Liar. The paradox remains a productive test for theories of truth, meaning and logical consequence, and its study has led to some of the most important technical work in philosophical logic.
Avicenna's Modal Syllogistic: A Persian Contribution to the History of Logic
H. Mohammad Ghorbanian
Aims This article introduces the modal syllogistic of Avicenna (Ibn Sīnā, d. 1037) to readers trained in modern logic and explains why it remains one of the most original episodes in the history of the subject.
Approach The discussion is expository and historical. It sets out the problem Avicenna inherited from Aristotle's Prior Analytics, reconstructs the main features of his analysis of categorical and modal propositions, and follows the reception of his ideas in later logic written in Arabic and Persian.
Main Points Avicenna's central move was to make the truth conditions of propositions explicit, in particular the temporal conditions under which a predicate belongs to a subject. His distinction between the substantial and the descriptive readings of a proposition, together with his broad reading of the subject term, explains the asymmetries of Aristotle's modal syllogisms that had puzzled earlier commentators. The same attention to truth conditions shaped his theory of quantified conditional propositions.
Conclusion Avicenna's logic is not a museum piece. It shows how careful semantic analysis can decide questions of validity, it shaped centuries of teaching in Iran and beyond, and it continues to repay formal study.
View Abstract
Approach The discussion is expository and historical. It sets out the problem Avicenna inherited from Aristotle's Prior Analytics, reconstructs the main features of his analysis of categorical and modal propositions, and follows the reception of his ideas in later logic written in Arabic and Persian.
Main Points Avicenna's central move was to make the truth conditions of propositions explicit, in particular the temporal conditions under which a predicate belongs to a subject. His distinction between the substantial and the descriptive readings of a proposition, together with his broad reading of the subject term, explains the asymmetries of Aristotle's modal syllogisms that had puzzled earlier commentators. The same attention to truth conditions shaped his theory of quantified conditional propositions.
Conclusion Avicenna's logic is not a museum piece. It shows how careful semantic analysis can decide questions of validity, it shaped centuries of teaching in Iran and beyond, and it continues to repay formal study.
Why Teach Logic? Reflections on Logic Education in Schools and Universities
F. Ranjbari
Aims This article asks what logic education is for, what research says about its effects, and how logic teaching in schools and universities, particularly in Iran, might be improved.
Approach The article reviews three common justifications for teaching logic, examines evidence from the psychology of reasoning and from mathematics education on what students learn from logic courses, and considers the current place of logic in Iranian curricula. It ends with practical proposals.
Main Points Logic is commonly taught in order to improve reasoning in general, to support the study of mathematics and computer science, and as part of a liberal and philosophical education. Research shows that formal logic courses do not automatically improve everyday reasoning, but that well-designed teaching that connects formal rules with meaningful contexts can have real effects. Students' difficulties with implication and quantifiers are a major obstacle in learning mathematical proof.
Conclusion Logic deserves a secure place in education, but its value depends on how it is taught. Integrating traditional and modern logic, teaching for transfer, using software tools and investing in teacher preparation are the main priorities.
View Abstract
Approach The article reviews three common justifications for teaching logic, examines evidence from the psychology of reasoning and from mathematics education on what students learn from logic courses, and considers the current place of logic in Iranian curricula. It ends with practical proposals.
Main Points Logic is commonly taught in order to improve reasoning in general, to support the study of mathematics and computer science, and as part of a liberal and philosophical education. Research shows that formal logic courses do not automatically improve everyday reasoning, but that well-designed teaching that connects formal rules with meaningful contexts can have real effects. Students' difficulties with implication and quantifiers are a major obstacle in learning mathematical proof.
Conclusion Logic deserves a secure place in education, but its value depends on how it is taught. Integrating traditional and modern logic, teaching for transfer, using software tools and investing in teacher preparation are the main priorities.
Logic Meets Computation: From the Curry--Howard Correspondence to Proof Assistants
A. Mirsanei
Aims This article explains the correspondence between proofs and programs known as the Curry--Howard correspondence, and shows how it has led to proof assistants that are now used to verify both mathematics and software.
Approach Starting from natural deduction and the simply typed lambda calculus, the article sets out the correspondence between propositions and types, proofs and programs, and proof normalization and evaluation, follows its main extensions, and reviews the leading proof assistants and their applications.
Main Points The correspondence is not an analogy but a precise structural identity: a proof in intuitionistic natural deduction is a typed program, and simplifying the proof is running the program. Dependent types extend the correspondence to quantifiers and allow mathematical statements and their proofs to be written and checked in a single language.
Conclusion The correspondence has turned an abstract result of logic into a practical technology that has verified major theorems and critical software.
View Abstract
Approach Starting from natural deduction and the simply typed lambda calculus, the article sets out the correspondence between propositions and types, proofs and programs, and proof normalization and evaluation, follows its main extensions, and reviews the leading proof assistants and their applications.
Main Points The correspondence is not an analogy but a precise structural identity: a proof in intuitionistic natural deduction is a typed program, and simplifying the proof is running the program. Dependent types extend the correspondence to quantifiers and allow mathematical statements and their proofs to be written and checked in a single language.
Conclusion The correspondence has turned an abstract result of logic into a practical technology that has verified major theorems and critical software.
Intuitionistic Logic and the Meaning of Proof
A. Valizadeh
Aims This article introduces intuitionistic logic as a philosophical position about the nature of mathematics and as a precise logical system, and explains why it remains central to the philosophy of mathematics and to computer science.
Approach The discussion follows the development of the subject from Brouwer's critique of classical reasoning, through Heyting's formalization and the proof interpretation of Brouwer, Heyting and Kolmogorov, to Kripke's semantics and Dummett's meaning-theoretic arguments.
Main Points Intuitionistic logic arises when the meaning of a mathematical statement is explained by what counts as a proof of it rather than by truth conditions that may transcend our knowledge. On this view the law of excluded middle is not a logical law, while most of ordinary reasoning remains valid. Classical and intuitionistic logic are closely related by translations, and intuitionistic logic has natural semantics in terms of growing states of knowledge.
Conclusion Intuitionism is not only a historical episode in the foundations of mathematics. Its central idea, that meaning is given by proof, remains a live option in the philosophy of language and underlies modern constructive mathematics and type theory.
View Abstract
Approach The discussion follows the development of the subject from Brouwer's critique of classical reasoning, through Heyting's formalization and the proof interpretation of Brouwer, Heyting and Kolmogorov, to Kripke's semantics and Dummett's meaning-theoretic arguments.
Main Points Intuitionistic logic arises when the meaning of a mathematical statement is explained by what counts as a proof of it rather than by truth conditions that may transcend our knowledge. On this view the law of excluded middle is not a logical law, while most of ordinary reasoning remains valid. Classical and intuitionistic logic are closely related by translations, and intuitionistic logic has natural semantics in terms of growing states of knowledge.
Conclusion Intuitionism is not only a historical episode in the foundations of mathematics. Its central idea, that meaning is given by proof, remains a live option in the philosophy of language and underlies modern constructive mathematics and type theory.
Gödel's Incompleteness Theorems: What They Do and Do Not Show
N. Roshandel Tavana
Aims This article gives a precise but accessible account of Gödel's two incompleteness theorems and separates what they establish from the many claims that are made in their name.
Approach The theorems are stated carefully for effectively axiomatized theories of arithmetic. The main steps of the proof (arithmetization, representability and the diagonal lemma) are explained informally, and the later strengthenings due to Rosser, Hilbert, Bernays and Löb are described.
Main Points The first theorem shows that no consistent, effectively axiomatized theory that contains a modest amount of arithmetic can decide every arithmetical sentence. The second shows that such a theory cannot prove its own consistency. Both results depend essentially on their hypotheses. They do not imply that every formal system is incomplete, that mathematical truth is unknowable, that we cannot be confident of the consistency of arithmetic, or that the human mind cannot be a machine.
Conclusion The incompleteness theorems are precise statements about formal theories. Read correctly, they mark a lasting limit on the axiomatic method and open several of the most fruitful directions in modern logic.
View Abstract
Approach The theorems are stated carefully for effectively axiomatized theories of arithmetic. The main steps of the proof (arithmetization, representability and the diagonal lemma) are explained informally, and the later strengthenings due to Rosser, Hilbert, Bernays and Löb are described.
Main Points The first theorem shows that no consistent, effectively axiomatized theory that contains a modest amount of arithmetic can decide every arithmetical sentence. The second shows that such a theory cannot prove its own consistency. Both results depend essentially on their hypotheses. They do not imply that every formal system is incomplete, that mathematical truth is unknowable, that we cannot be confident of the consistency of arithmetic, or that the human mind cannot be a machine.
Conclusion The incompleteness theorems are precise statements about formal theories. Read correctly, they mark a lasting limit on the axiomatic method and open several of the most fruitful directions in modern logic.
Indexing and Abstracting
