5

I have been wondering where the form enter image description here

originates from. The turnstile ⊢ famously comes from Frege, but I haven't been able to find where the vertical notation was introduced. In the field of Programming Languages, the horizontal bar is used in a similar way, but is probably stolen for convenience, and isn't used in the same manner. It is also distinct from this style, as the premises of the rule are laid out horizontally.

4
  • 3
    My best bet would be Gentzen, or proof theory anyway, but I don't know that for sure. Nov 7, 2023 at 2:09
  • 2
    The horizontal bar is called the inference line and seems to have been introduced by Gentzen. Listing sentences vertically is ancient. The turnstile in modern logic is derived from Frege's assertion symbol, but it is not the same thing. The turnstile indicates derivability, while the turnstile marks that a sentence is asserted as true.
    – Bumble
    Nov 7, 2023 at 2:32
  • 2
    According to MacTutor the therefore symbol is the oldest (Rahn, 1659), p as a propositional variable (Peano, 1897), p, q, r as propositional variables (Russell, 1903), and the implication symbol (Hilbert, 1922). So your exact scheme must postdate 1922 and Gentzen seems a likely candidate.
    – nwr
    Nov 7, 2023 at 3:42
  • The system used in Programming Languages is less distinct than you think -- it's Gentzen-style "natural deduction." en.wikipedia.org/wiki/Natural_deduction Nov 7, 2023 at 19:25

1 Answer 1

7

As per comments above, the modern use is due to Hilbert's school.

Gerhard Gentzen, Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen (1932) derived it from Paul Hertz, Über Axiomensysteme für beliebige Satzsysteme I, Math. Ann. 87 (1922):

I.a→bII.b→cIII.a→c

and David Hilbert, Die logischen Grundlagen der Mathematik. (1922), page 152 (the "canonical" representation of Modus Ponens).

And see Hilbert's 1920 Lectures into David Hilbert, Lectures on the Foundations of Arithmetic and Logic. 1917-1933 (Springer, 2013).

Already G.Frege (1879) proposed to represent inferences with the horizontal line:

enter image description here

1
  • I think I came across it differently Nov 7, 2023 at 8:54

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .