Take a first order language with Parameter:

Constant Symbol: $\emptyset$

Equality Relation and Belonging to Relation as Predicate Symbol

Now take theory in this first order language with axioms:

  1. $(\forall x)(\forall y)\Bigg((x=y) \longleftrightarrow \Big((\forall z)(z \in x \longleftrightarrow z \in y)\Big)\Bigg)$

  2. $(\forall x)(\forall y)\Bigg((x\neq y) \longleftrightarrow \Big((\exists z)\big(z \in x \land z \notin y)\lor (z \notin x \land z \in y)\big)\Big)\Bigg)$

  3. $(\forall x)(\forall y)(\forall z)\Big(\big(x=y) \land (x \in z)\big) \longrightarrow (y \in z)\Big)$

  4. $(\forall x)(x \notin \emptyset)$

Question: Is this theory consistent?

Explanation of terms: Consistency means prove there doesn't exist $\phi$ such that this theory proves $\phi$ as well as $\neg\phi$.

Consistency I am not taking whether there exist model of this theory in set theory.

  • $\begingroup$ Hint: There is a model with one element. $\endgroup$ – Henning Makholm Mar 18 '16 at 17:08
  • $\begingroup$ @Sushil Regarding "Consistency means prove there doesn't exist $\varphi$ such that this theory proves $\varphi$ as well as $\lnot\varphi$. Consistency I am not taking whether there exist model of this theory in set theory." First-order logic is sound for its usual semantics. A consequence of this is that if we can produce a model of a theory $T$, then $T$ is consistent. Indeed, if we could prove $\varphi$ and $\lnot\varphi$ from $T$, then both would be true in a model $M\models T$, which is impossible. $\endgroup$ – Alex Kruckman Mar 18 '16 at 17:31
  • $\begingroup$ Okay but can we prove directly it is consistent without using that existence of model arguement @AlexKruckman $\endgroup$ – Sushil Mar 18 '16 at 17:34
  • 2
    $\begingroup$ I wouldn't recommend it! $\endgroup$ – Alex Kruckman Mar 18 '16 at 17:36
  • 3
    $\begingroup$ @Sushil: You can disguise the model-theoretic argument as a syntactic one if you desperately want to: You can write down a purely syntactic definition by structural recursion, defining of a class of formulas that happens to coincide with the formulas that are true in $\{\{\varnothing\},{\in}\}$. Then prove that each of your axioms are in the class you have defined, and that the class is closed under each of the rules of inference of your logic. Conclude that every provable formula is in the class, and note that the class does not contain both $\phi$ and $\neg\phi$ for any $\phi$. $\endgroup$ – Henning Makholm Mar 18 '16 at 17:39

Yes - for example, it is true in the structure with a single element $E$ (for emptyset), and where the binary relation is empty. It also has less stupid examples: given any transitive set $X$, the pair $(X, \in)$ is a model of this theory.

(Note that having a model easily implies consistency - this is the soundness theorem. More surprisingly, the converse is also true - this is the completeness theorem.)

Based on this, I'm not really sure you wrote the axioms you intend. Also, unless I'm misreading, (2) is the same as (1), and (3) follows from the semantics of equality in first-order logic. Did you mean to write other axioms?

  • $\begingroup$ It doesn't follow solely from there being no existential quantifiers. For example the theory $\{(\forall x)(x\in x), (\forall x)(x\notin x)\}$ is not consistent. $\endgroup$ – Henning Makholm Mar 18 '16 at 17:10
  • $\begingroup$ @HenningMakholm Good point, fixed. $\endgroup$ – Noah Schweber Mar 18 '16 at 17:12
  • $\begingroup$ I think the theory is meant to work in a logic where equality is not a logical primitive (in other words, there are no logical axioms for $=$). Then axiom 3 together with 1 (or 2) guarantee that the $=$ predicate actually behaves like equality should. $\endgroup$ – Henning Makholm Mar 18 '16 at 17:13
  • 2
    $\begingroup$ @Sushil: As Noah remarks, your theory has a model. You should already know that a theory that has a model is consistent (because every formula the theory can prove will be true in the model and it is impossible by definition for both $\phi$ and $\neg\phi$ to be true in the same structure) -- that is a consequence of the soundness theorem and is the most important way to prove that a theory is consistent. $\endgroup$ – Henning Makholm Mar 18 '16 at 17:32
  • 3
    $\begingroup$ @Sushil: Your axiom 3 is one of the usual logical axioms for equality, so if your logic treats equality as a primitive, you don't even need to list it as an axiom. (And, as Noah notes, your axioms 1 and 2 are logically equivalent). $\endgroup$ – Henning Makholm Mar 18 '16 at 17:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.