The relations $A \vdash B$, read "$A$ proves $B$'', and $A\vDash B$, read if $A$ is true then $B$ is true, are referred to as syntactic and semantic consequence, respectively.

In the history of mathematics, who introduced these concepts first? It seems clear that Aristotle studied $A\vDash B$ in one way or another, and that the Stoics developed the "connectives" of this relation: introducing $B\wedge C$, $B\vee C$, etc. If this is correct, then who first developed syntactic consequence?

  • $\begingroup$ Nobody introduced these concepts "first". There were three different conceptions of semantic consequence already in the middle ages, all of them with some motivation from Aristotle. And neither Aristotle nor scholastics nor Leibniz clearly distinguished between those and 'syntactic' consequence, which would be employing syllogism figures, although they did that too and some even attempted to 'syllogize' Euclid. The semantic/syntactic distinction was not fully fleshed out until Gödel and Tarski, but it is hard to call them "first" either. $\endgroup$
    – Conifold
    Commented May 30 at 6:42
  • $\begingroup$ The first modern example of proof system is due to Frege (1879). Prior to it, both Boole and Peano were not clear enough about the distinction between axioms and rules. $\endgroup$ Commented May 30 at 7:29
  • $\begingroup$ See Ivor Grattan-Guinness, The Search for Mathematical Roots 1870-1940. Logics set theories and the foundations of mathematics from Cantor through Russell to Gödel (Princeton UP, 2000), page 44: "Boole was not primarily concerned with laying out deductions from his premises in the meticulous way that Frege, Russell and the mathematical logicians have accustomed us to expect, but rather to find their consequences by means of algebraic manipulations." $\endgroup$ Commented May 30 at 14:00
  • $\begingroup$ Compare with Frege (1896): "The number of means of inference will be reduced as much as possible and these will be put forward as rules of this new language. This is the fundamental thought of my concept script." (Same reference above, page 179). $\endgroup$ Commented May 30 at 14:00
  • $\begingroup$ @MauroALLEGRANZA "Arithmetices principia, nova methodo exposita" is written later (1889), but according to Jan von Plato "Peano’s derivations are constructed purely formally, with a notation as explicit as one could desire, by the application of axiom instances and implication eliminations". I suppose Peano's system of rules was "à la Hilbert". $\endgroup$
    – M. Lonardi
    Commented May 30 at 14:35


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.