New answers tagged

3

Let $S$ be a sentence symbol, and let $\varphi$ be $\neg S$; then $\varnothing\not\vDash S$, since $S\notin\varnothing$, so $\varnothing\vDash\varphi$.


9

You have in fact used a weak form of the axiom of choice, specifically, the axiom of dependent choice. Without choice you can make any finite number of arbitrary choices, but you cannot in general make an infinite sequence of them.


4

Can I try an alternative angle on this that may help. In a theory like ZF, you cannot construct a model of ZF, but you can give a perfectly rigorous definition of what is to be a model of a first-order theory like ZF. To coin a pun, ZF doesn't know much about the art of constructing models, but it knows a good model when it sees one. From this point of view, ...


3

Cohen showed that if $M$ is a countable transitive model of $V=L$,1 then there is another, larger model, $M[G]$, which is also countable and transitive, has the same ordinals as $M$, and in $M[G]$ the Continuum Hypothesis fails. Indeed, a model is simply a set with a binary relation, and in Cohen's case, it is a [countable] transitive set in some ambient ...


2

As Don Thousand and Mauro ALLEGRANZA pointed out, there are ways to circumvent the need for a provability predicate. A systematic method to go about constructing true but unprovable statements would use that every theory has an ordinal strength $\alpha$, then construct a set $S$ which is well ordered, with order type $\beta\ge\alpha$. Then, encode the ...


0

Complementary to Robert's answer, you might like to be aware of the proofs-as-programs or propositions-as-types paradigm, also known as the Curry-Howard correspondence. Under this correspondence, a logical statement (such as $\alpha \to (\beta \to \alpha)$) corresponds to a program (or function) that represents a proof of that statement (such as $x \mapsto y ...


2

Some proofs are of a very different style from others; geometrical vs algebraic vs formal vs generalized, etc. Technically everything known in mathematics can be proven from the axioms; that doesn't mean those theorems are all superfluous. One gauge of a mathematician's breadth of knowledge is how many totally different proofs of the Pythagorean theorem they ...


2

Long comment IMO, you are "reading too much" in the specific quote. Wittgenstein is a difficult philosopher: its style is idiosyncratic, the books of so-called second period has been published posthumously and most of them are from notes taken from Wittgenstein's lectures. You can see Georg Kreisel's Review of Remarks on the Foundations of ...


2

This is very late to the party, but I think it's worth noting that there are in fact specific obstacles to finding "natural" nonstandard models of set theories, coming from computability theory. To start with, we have: There is no computable model of $\mathsf{ZF}$. (The argument here works for other set theories like $\mathsf{NFU}$ as well, it's ...


0

I know this is a pretty old post, but I want to share some of my own insights. First, I want to highlight a slight error in the answer by mercio. It is a correct model of PA - induction, but Robinson Arithmetic is PA - induction + $\forall n (n = 0 \vee \exists m (n = S(m)))$. Their model does not satisfy this additional axiom, as $X$ does not have a ...


0

There is a way to define the natural numbers directly. Unlike the standard definition, it is not self-referential in nature. Before getting to that, I will review the standard definition. The most well-known construction of the natural numbers, found in texts such as those by Enderton or Hrbacek and Jech, begins as follows: An inductive set is any set $X$ ...


1

Building $\Bbb Z$ and establishing basic properties of arithmetic starting with just the axioms of ZFC is a complex task (e.g. one rigorous formal proof that $2+2=4$ is almost 3,000 steps long)! This process includes introducing notation and terminology for numbers and numeric operations (defined in terms of set operations) and proving useful theorems (e.g. ...


4

Asking how to prove a theorem about $m^2$ in $\Bbb Z$ using $\sf ZFC$ is similar to asking how to write a JavaScript interpreter from complete scratch, in machine code. It's not that it's not possible, but it's just that this is not what you're supposed to do if you want to write a JavaScript interpreter. For one, it's a lot easier to use an operating system ...


3

The most introductory material related to ETCS is Trimble’s informal notes starting here: https://ncatlab.org/nlab/show/Trimble+on+ETCS+I However, this may not be introductory enough, depending on your background, since you say you’re quite new to category theory. Leinster’s book Basic Category Theory is where’d I’d usually send an undergraduate (my best ...


Top 50 recent answers are included