Talk:Disjunction and existence properties

Charles matthew's number theoretic conjecture

The number theory example I'm thinking of is a quite striking one about primitive roots. Charles Matthews 19:30, 23 Sep 2004 (UTC)

A quibble

In particular the existence property is fundamental to understanding in what sense proofs can be considered to have content: the essence of the discussion of existence theorems.

Herbrand's theorem, in its original form and for many classical theories, tells us something weaker than the existence property; namely it tells us that for some t1 ... tn, phi(t1) \/ ... \/ phi(tn) is a theorem, so any model must identify which of those ti is the (a) witness. I think Herbrand's theorem does establish that the proof has content, in the sense you describe, for non-constructive theories. Oh, and I'd like to hear more about your number theoretic example. ---- Charles Stewart 11:37, 24 Sep 2004 (UTC)

So, it would be good to have discussion of the proof theory : both Herbrand's theorem, and also the argument that in a cut-free proof with last line proving a disjunction, the penultimate line must prove a disjunct (sorry if I'm putting this badly - my knowledge of the field is a bit amateurish). Primitive roots - I'm thinking of the approximation to the Artin conjecture which says that, at least one out of 2, 3, 5 is a primitive root modulo infinitely many primes: but we can't know which. I have thought for a while that a logician's commentary on this would be interesting, and less hackneyed than some of the other examples of non-constructive techniques and possible 'proof unwinding'. Charles Matthews 12:46, 24 Sep 2004 (UTC)

---

• also the argument that in a cut-free proof with last line proving a disjunction, the penultimate line must prove a disjunct

In fact this isn't a theorem (I assumke you're talking about the sequent calculus): in LK the last rule applied can be a contraction, which is why the disjunction property can't be proven for LK;

• at least one out of 2, 3, 5 is a primitive root modulo infinitely many primes: but we can't know which.

I don't know the conjecture (I've heard of the Artin conjecture, but I can't recall what it's about, should read more wikipedia, I guess), but it looks like this would be an excellent addition to the page ---- Charles Stewart 16:49, 24 Sep 2004 (UTC)

According to the article Artin's conjecture on primitive roots, the candidates are {3, 5, 7}. It says the proof is non-constructive, fine... but you claim, "we can't know which", and I can't tell if you mean to say that Heath-Brown somehow proved that it's undecidable (?) or if it's simply unknown as yet. --Jorend 20:10, 29 November 2006 (UTC)

Examples

From the article:

There are quite concrete examples in number theory where this has a major effect.

I think it would be helpful to give two or so examples of this. CRGreathouse (t | c) 23:27, 7 February 2007 (UTC)

The formulas must be sentences

I added the word "sentence" (closed formula) to the disjunction property and to the existence property. About the disjunction property, I think that it doesn't hold (at least in some versions of) Heyting arithmetic if the formula $\phi \vee \psi$ isn't closed: for example, (a version of) Heyting arithmetic proves $x=0\vee x\neq 0$ but doesn't prove $x=0$ and doesn't prove $x\neq 0$. About the existence property, I think that is just a matter of convention to assume that the formula $\exists x\colon \phi (x)$ is closed. (I'm assuming that the term theorem doen't imply that the formula is closed — I hope that I got this right). Jayme 15:44, 9 August 2007 (UTC)

Existence property of IZF

John Myhill (1973) showed that IZF with the axiom of Replacement eliminated in favor of the axiom of Collection has the disjunction property, the numerical existence property, and the existence property.

What does it mean? If I understand it correctly, the language of IZF has no function symbols (including constants) in its signature. Thus, the only kind of terms are variables. Existence property declares, that for the theorem $\exists x~\varphi (x)$ the theorem $\varphi (t)$ exists, where $t$ is some term. But "some term" can only be a variable. Therefore, the theorem $\varphi (x)$ exists. What's wrong?

Eugepros (talk) 12:01, 13 April 2018 (UTC)