I have a question regarding \equiv and \iff . If I want to prove that\{x| \phi(x)\} = \{x| \psi(x)\}, then should I say that \phi(x) \equiv \psi(x), or \phi(x) \iff \psi(x) ?
\{x| \phi(x)\} and \{x| \psi(x)\} are sets that have the same elements
My point of confusion comes from the Axioms of Equality, from which I could surely say \phi(x) \iff \psi(x) ; but I think that to replace the predicate I would need \phi(x) \equiv \psi(x)
I tend to think \equiv and \iff are the same (at least for a problem of this kind), but I feel unsure about changing a symbol for one I think is intuitively the same
Note: "My point of confusion comes from the Axioms of Equality, from which I could surely say \phi(x) \iff \psi(x)" I mean using other info given
@Cure "iff" is English short-hand for "if and only if". We may use the symbol "≡" or "⇔" for "iff".
But I don't understand the rest of your question, and it sounds like a basic misconception about equality. You should state what you thought "axioms of equality" are.
This is an excellent question! Basically, you are asking for ways to cut down the search space for finding a proof within some formal system. To be concrete let us say that you use this Fitch-style natural deduction system. Then the following hold within any subcontext:
If you can deduce $A∧B$, ...
@Threnody: The above post may be helpful for you. I decided to write it down, thanks to some new user who posted such a great question!
@user21820 this is a funny attempt, but I am not convinced:
LEM<A=>B>
LEM<B=>A>
If ¬(B=>A)
LEM<B=>A>
LEM<B=>A> or conc
¬(B=>A) => LEM<B=>A> or conc
If B=>A
LEM<B=>A>
LEM<B=>A> or conc
B=>A => LEM<B=>A> or conc
LEM<B=>A> or conc
B=>A or ¬(B=>A) or B=>A or A=>B
//magically erase LEM<B=>A> :D
conc
Here LEM<X> is shorthand for X v ¬X
Intuitively I know X v ¬X is a tautology, but how do I go about erasing it when in disjunction with something else?
No... this isn't right...
I can't just erase what's possibly the only true part of a disjunction
