Timeline for Examples of anti-classical theories in iFOL
Current License: CC BY-SA 4.0
28 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 11 at 16:31 | comment | added | user76284 | @EmilJeřábek I see: ¬(ϕ∨¬ϕ) ⇒ (ϕ∨¬ϕ)→⊥ ⇒ (ϕ→⊥)∧(¬ϕ→⊥) ⇒ (ϕ→⊥)∧((ϕ→⊥)→⊥) ⇒ ⊥. | |
| Nov 2 at 21:21 | comment | added | Emil Jeřábek | @user76284 Intuitionistic logic proves $\neg\neg(\phi\lor\neg\phi)$. | |
| Nov 2 at 20:24 | comment | added | user76284 | @EmilJeřábek "A theory that proves ¬(ϕ∨¬ϕ) is not just anti-classical, but inconsistent." How so? | |
| Oct 30 at 16:13 | comment | added | James E Hanson | @AndrejBauer Regarding many-sorted theories, for theories with finitely many sorts, don't the standard classical model theory tricks of coding functions as relations and coding sorts as disjoint (decidable) sets still work intuitionistically? In other words, isn't it still true that every theory with finitely many sorts is biinterpretable with a single-sorted (relational) theory? What tricks don't work exactly? | |
| Oct 30 at 15:17 | vote | accept | Jason Carr | ||
| Oct 30 at 12:15 | answer | added | Emil Jeřábek | timeline score: 9 | |
| Oct 30 at 9:19 | comment | added | Andrej Bauer | @EmilJeřábek: It would be worth posting ECT (phrased as a schema) as an answer, I think. | |
| Oct 30 at 8:12 | comment | added | Emil Jeřábek | @JasonCarr Sure, as mentioned above, CT (which is a schema like the ECT written above, but without $\psi$) implies this e.g. when $P$ is a $\Sigma_1$-complete predicate such as $\{e\}(x)\simeq y$ (encode the triple $\langle e,x,y\rangle$ with a single number $n$ if you wish). | |
| Oct 30 at 8:05 | comment | added | Emil Jeřábek | @AndrejBauer I'm sure higher-order people use it in ways I am not familiar with, but in the context of first-order arithmetic, no, ECT is just a first-order axiom schema: $\forall x\,(\psi(x)\to\exists y\,\phi(x,y))\to\exists e\,\forall x\,(\psi(x)\to\exists y\,(\{e\}(x)\simeq y\land\phi(x,y)))$, where $\psi$ is essentially negative, and $\{e\}(x)\simeq y$ denotes a $\Sigma_1$ formula expressing "the program with code $e$ computes $y$ on input $x$". | |
| Oct 29 at 23:54 | comment | added | Jason Carr | Allegedly there are some extensions like: $\textbf{HA} + \neg \forall n, (P(n) \vee \neg P(n))$ which are consistent (and anti-classical), but I haven't found details for these yet. Interestingly the form of this is quite similar to the example above (since $\forall n, \neg\neg (P(n) \vee \neg P(n))$ is trivially true) | |
| Oct 29 at 22:38 | comment | added | Andrej Bauer | But I think ECT wouldn't count according to the OP since it quantifies over functions $\mathbb{N} \to \mathbb{N}$, would it? | |
| Oct 29 at 22:37 | comment | added | Emil Jeřábek | A non-artificial example of an anticlassical theory is HA + CT (or its extentions like ECT). | |
| Oct 29 at 22:31 | comment | added | Emil Jeřábek | On second thoughts, just $n=1$ suffices, i.e., a theory is anticlassical iff it proves $\neg\forall\vec x\,(\phi(\vec x)\lor\neg\phi(\vec x))$ for some formula $\phi(\vec x)$. The reduction from the form above is to take for $\phi(\vec x)$ the formula $\bigwedge_i(\phi_i(\vec x)\lor\neg\phi_i(\vec x))$ (whose negation is provably false). | |
| Oct 29 at 22:14 | comment | added | Andrej Bauer | Oops, a rookie mistake! Anyhow, it does seem difficult to come by reasonable anti-classical first-order theories. Interesting. | |
| Oct 29 at 21:45 | comment | added | Jason Carr | I was about to ask exactly that question. I reworded it to be vaguer so as to be correct, but we definitely need to use formulas with free variables, and was wondering if it suffices to only use one formula or possibly multiple | |
| Oct 29 at 21:44 | history | edited | Jason Carr | CC BY-SA 4.0 |
deleted 4 characters in body
|
| Oct 29 at 21:42 | comment | added | Emil Jeřábek | @AndrejBauer A theory that proves $\neg(\phi\lor\neg\phi)$ is not just anti-classical, but inconsistent. Anyway, I think the intent is clear: a formula $\phi$, or a theory $T$ if you wish, is anticlassical if it is inconsistent with classical logic, i.e., if $\mathrm{LEM}\cup T\vdash\bot$ to use a more formally correct notation. This amounts to $T\vdash\neg\bigwedge_{i<n}\forall\vec x\,(\phi_i(\vec x)\lor\neg\phi_i(\vec x))$ for some formulas $\phi_i$. | |
| Oct 29 at 21:13 | comment | added | Andrej Bauer | Also, you should allow multi-sorted theories here, because in intuitionsitic logic we cannot play tricks that reduce multi-sorted theories to single-sorted ones. | |
| Oct 29 at 21:12 | comment | added | Andrej Bauer | Since you are careful about first-order vs. higher-order, what is $LEM$ in $\phi \land LEM \vdash \bot$? In first-order logic LEM would be a schema, not a formula, but then your characterization of anti-classical is not well formed. Wouldn't it be better to just say that a theory (as opposed to an axiom) is anti-classical if it proves $\neg (\phi \lor \neg \phi)$ for at least one formula $\phi$? | |
| Oct 29 at 21:08 | comment | added | Jason Carr | I adjusted the question to clarify what anti-classical means here. It is different from non-classical (i.e. not-necessarily-classical) | |
| Oct 29 at 21:05 | history | edited | Jason Carr | CC BY-SA 4.0 |
added 85 characters in body
|
| Oct 29 at 20:42 | comment | added | Jason Carr | Yes, not all theories extend this. This is a distinct theory from the theory of Heyting Arithmetic. It is already inconsistent because HA proves that $0 \not = 1$, regardless of the proofs of LEM, but that's inconsistent with $\forall x y, \neg (x \neq y)$ | |
| Oct 29 at 19:11 | comment | added | Hanul Jeon | Also I do not think every anti-intuitionistic theory satisfies what you mentioned; For example, $\mathsf{HA}$ proves LEM for $\Delta_0$-formulas, so for every binary predicate symbol $R$ in the language of $\mathsf{HA}$ (either $\{<,=\}$ or the set of all primitive recursive binary relations) we have $\lnot\lnot R(x,y)\to R(x,y)$. In particular, it is impossible that both $\forall x,y \lnot\lnot R(x,y)$ and $\lnot \forall x,y R(x,y)$ hold for an atomic binary predicate $R$. However, there are non-classical models of $\mathsf{HA}$... | |
| Oct 29 at 18:59 | comment | added | Jason Carr | "A sort like this" meaning of the form: adding some relation-symbol and exploiting a similar condition on quantifiers. This is a question about the theory, not the models, so I'm not sure the question about Grothendieck vs. non-Grothendieck is relevant. AFAIK there's a completeness theorem that Grothendieck topoi always suffice (take the syntactic topos) | |
| Oct 29 at 18:55 | comment | added | Hanul Jeon | "a sort like this" sounds a bit ambiguous making the answer hard to state. What do you mean for that? Also, the previous version of your question seems to suggest you are only considering Grothendieck toposes, but there are non-classical elementary toposes (like, realizability toposes) | |
| Oct 29 at 18:50 | history | edited | Jason Carr | CC BY-SA 4.0 |
deleted a bad example
|
| S Oct 29 at 18:32 | review | First questions | |||
| Oct 29 at 21:19 | |||||
| S Oct 29 at 18:32 | history | asked | Jason Carr | CC BY-SA 4.0 |