Editing Temporal logic (section)

== Łoś's positional logic ==
[[Jerzy Łoś|Łoś]]’s logic was published as his 1947 master’s thesis ''Podstawy Analizy Metodologicznej Kanonów Milla'' (''The Foundations of a Methodological Analysis of Mill’s Methods'').<ref name="Tkaczyk 2019 259–276">{{Cite journal|last1=Tkaczyk|first1=Marcin|last2=Jarmużek|first2=Tomasz|date=2019|title=Jerzy Łoś Positional Calculus and the Origin of Temporal Logic|journal=Logic and Logical Philosophy|language=en|volume=28|issue=2|pages=259–276|doi=10.12775/LLP.2018.013|issn=2300-9802|doi-access=free}}</ref> His philosophical and formal concepts could be seen as continuations of those of the [[Lviv–Warsaw School of Logic]], as his supervisor was [[Jerzy Słupecki]], disciple of [[Jan Łukasiewicz]]. The paper was not translated into English until 1977, although [[Henryk Hiż]] presented in 1951 a brief, but informative, review in the ''[[Journal of Symbolic Logic]]''. This review contained core concepts of [[Jerzy Łoś|Łoś]]’s work and was enough to popularize his results among the logical community. The main aim of this work was to present [[Mill's canons]] in the framework of formal logic. To achieve this goal the author researched the importance of temporal functions in the structure of Mill's concept. Having that, he provided his axiomatic system of logic that would fit as a framework for [[Mill's canons]] along with their temporal aspects.

=== Syntax ===
The language of the logic first published in ''Podstawy Analizy Metodologicznej Kanonów Milla'' (''The Foundations of a Methodological Analysis of Mill’s Methods'') consisted of:<ref name=":0" />

* first-order logic operators ‘¬’, ‘∧’, ‘∨’, ‘→’, ‘≡’, ‘∀’ and ‘∃’
* realization operator U
* functional symbol δ
* propositional variables p<sub>1</sub>,p<sub>2</sub>,p<sub>3</sub>,...
* variables denoting time moments t<sub>1</sub>,t<sub>2</sub>,t<sub>3</sub>,...
* variables denoting time intervals n<sub>1</sub>,n<sub>2</sub>,n<sub>3</sub>,...

The set of terms (denoted by S) is constructed as follows:

* variables denoting time moments or intervals are terms
* if <math>\tau \in S</math> and <math>\epsilon</math> is a time interval variable, then <math>\delta(\tau, \epsilon) \in S</math>

The set of formulas (denoted by For) is constructed as follows:<ref name="Tkaczyk 2019 259–276"/>

* all first-order logic formulas are in <math>For</math>
* if <math>\tau \in S</math> and <math>\phi</math> is a propositional variable, then <math>U_{\tau}(\phi) \in For</math>
* if <math>\phi \in For</math>, then <math>\neg \phi \in For</math>
* if <math>\phi, \psi \in For</math> and <math>\circ \in \{\wedge, \vee, \rightarrow, \equiv\}</math>, then <math>\phi \circ \psi \in For</math>
* if <math>\phi \in For</math> and <math>Q \in \{\forall, \exists\}</math> and υ is a propositional, moment or interval variable, then <math>Q_{\upsilon}\phi \in For</math>

=== Original Axiomatic System ===

# <math>U_{t_{1}}\neg p_{1} \equiv \neg U_{t_{1}} p_{1}</math>
# <math>U_{t_{1}}(p_{1} \rightarrow p_{2}) \rightarrow (U_{t_{1}} p_{1} \rightarrow U_{t_{1}} p_{2})</math>
# <math>U_{t_{1}}((p_{1} \rightarrow p_{2}) \rightarrow ((p_{2} \rightarrow p_{3}) \rightarrow (p_{1} \rightarrow p_{3})))</math>
# <math>U_{t_{1}}(p_{1} \rightarrow (\neg p_{1} \rightarrow p_{2}))</math>
# <math>U_{t_{1}}((\neg p_{1} \rightarrow p_{1}) \rightarrow p_{1})</math>
# <math>\forall_{t_{1}}U_{t_{1}}p_{1} \rightarrow p_{1}</math>
# <math>\forall_{t_{1}}\forall_{n_{1}}\exists_{t_{2}}\forall_{p_{1}}(U_{\delta(t_{1},n_{1})} p_{1} \equiv U_{t_{2}}p_{1})</math>
# <math>\forall_{t_{1}}\forall_{n_{1}}\exists_{t_{2}}\forall_{p_{1}}(U_{\delta(t_{2},n_{1})} p_{1} \equiv U_{t_{1}}p_{1})</math>
# <math>\forall_{t_{1}}\exists_{p_{1}}\forall_{t_{2}}(U_{t_{2}} p_{1} 
\equiv \forall_{p_{2}}(U_{t_{1}}p_{2} \equiv U_{t_{2}}p_{2}))</math>