Search Results
Search type | Search syntax |
---|---|
Tags | [tag] |
Exact | "words here" |
Author |
user:1234 user:me (yours) |
Score |
score:3 (3+) score:0 (none) |
Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
Views | views:250 |
Code | code:"if (foo != bar)" |
Sections |
title:apples body:"apples oranges" |
URL | url:"*.example.com" |
Saves | in:saves |
Status |
closed:yes duplicate:no migrated:no wiki:no |
Types |
is:question is:answer |
Exclude |
-[tag] -apples |
For more details on advanced search visit our help page |
first-order and higher-order logic, model theory, set theory, proof theory, computability theory, formal languages, definability, interplay of syntax and semantics, constructive logic, intuitionism, philosophical logic, modal logic, completeness, Gödel incompleteness, decidability, undecidability, theories of truth, truth revision, consistency.
4
votes
3
answers
3k
views
First-order logic without equality and set theory
Is it possible to build set theory on first-order logic without equality?
For example, how could one show that if $x_0=x_1$ then $\left\{x_0\}=\{x_1\right\}$, where $x_0$ and $x_1$ are two sets? And …
1
vote
2
answers
2k
views
What does the disjunction elimination rule say?
I read about two different versions of the disjunction elimination rule.
The first version (http://www.fecundity.com/logic/) says that:
if $\Sigma\vdash\phi_0\lor\phi_1$ and $\Sigma\vdash\lnot\phi_ …
2
votes
3
answers
778
views
Does the axiom of specification prevent writing any proof?
In set theory, the axiom of specification says that $\forall x_0\exists x_1\forall x_2\left(x_2\in x_1\leftrightarrow x_2\in x_0\land\theta\left[x_2\right]\right)$, where $\theta\left[x_2\right]$ is a …
12
votes
7
answers
9k
views
Is there any proof assistant based on first-order logic?
I'm looking for a proof assistant in order to write formal proofs about basic facts of set theory, such as:
$a\subseteq a$
$(a,b)=(c,d)\leftrightarrow a=c\land b=d$
Natural deduction for first-ord …
14
votes
6
answers
5k
views
Do you know any good introductory resource on sequent calculus?
I'm looking for a good introductory resource on sequent calculus suitable for someone who has studied natural deduction before. Books and online resources are both OK, as long as each rule of inferenc …
1
vote
Accepted
Is reflexivity of equality an axiom or a theorem?
I managed to write down a proof for the reflexivity of equality using only the definition of equality in terms of membership and the rules of natural deduction.
Premise: $\forall x_0\forall x_1\left …
3
votes
2
answers
3k
views
Why are universal introduction and existential elimination valid inference rules?
I'm studying the inference rules of natural deduction for the first-order logic. I cannot understand why universal introduction and existential elimination are valid rules. The first one says that if …
4
votes
5
answers
3k
views
Is reflexivity of equality an axiom or a theorem?
Everybody knows that equality is reflexive: $\forall(x)(x=x)$. But should reflexivity of equality be taken as an axiom of logic or as a theorem of set theory?
If you choose the former then you probab …