Two Early Arabic Applications of Model-Theoretic Consequence

We trace two logical ideas further back than they have previously been traced. One is the idea of using diagrams to prove that certain logical premises do—or don’t—have certain logical consequences. This idea is usually credited to Venn, and before him Euler, and before him Leibniz. We find the idea correctly and vigorously used by Abū al-Barakāt in 12th century Baghdad. The second is the idea that in formal logic, P logically entails Q if and only if every model of P is a model of Q. This idea is usually credited to Tarski, and before him Bolzano. But again we find Abū al-Barakāt  already exploiting the idea for logical calculations. Abū al-Barakāt’s work follows on from related but inchoate research of Ibn Sīnā in eleventh century Persia. We briefly trace the notion of model-theoretical consequence back through Paul the Persian (sixth century) and in some form back to Aristotle himself.