« first day (490 days earlier)      last day (2344 days later) » 

3:45 AM
@user21820 is ZFC under two different encodings of ordered pairs equivalent?
 
@LeakyNun Equivalent in what sense? You mean that the axioms depend on the choice of ordered pairs, so you are asking whether one version of the axioms makes another version redundant? I am pretty sure it does not, and so the answer to your question is "no". But I can't be sure, so if you ask on Main let me know!
 
@user21820 by equivalent, I mean:
let $\varphi$ be a sentence over $L_{ZFC} = \{\in\}$. Then, $(ZFC^a \vDash \varphi) \iff (ZFC^b \vDash \varphi)$
 
Yea and I'm quite sure the answer is no.
Because for example you have the replacement schema, which states the existence of some function blah blah...
But that statement has to be expanded according to the choice of ordered pairs because a function is a set of ordered pairs...
 
let's say we only choose $a(x,y) = \{x,\{x,y\}\}$ and $b(x,y) = \{\{x\},\{x,y\}\}$?
 
Well, maybe I'm not so sure.
 
3:58 AM
that's a(x,y)={x,{x,y}} and b(x,y)={{x},{x,y}}
alright
 
Because I can imagine we could use one version and then unpack the ordered pair as needed.
 
@user21820 exactly
 
The closest I can find on Main about this issue is this:
4
Q: slightly different definition of an ordered pair

WillemienIn a paper I was reading an ordered pair had a slightly different definition $\langle a,b \rangle = \{a,\{a,b\}\}$ instead the normal Kuratowski definition which is that $\langle a,b \rangle = \{\{a\},\{a,b\}\}$. notice in the first one the $a$ is without braces. now I know that it is wrong , ...

Asaf suggests that some choices of ordered pair definitions make you have to use foundation to prove that they function as ordered pairs.
This means that without foundation you might have trouble with some definitions but not others.
I think there may be a related issue with the axiom of infinity. It is currently compatible with the von Neumann ordinal ω, but Zermelo at first proposed a different one, and the following answer suggests that you need replacement to get from Zermelo's to the modern one:
1
Q: Prove axiom of infinity from ZF$-$Infinity +Zermelo's version of infinity

user280486Assume ZF-infinity and assume that there is a set $X$ such that $\varnothing\in X$ and for all $t\in X$, $\{t\}\in X$. How to deduce axiom of infinity from these new axioms?

@LeakyNun: So I think that my original intuition should be correct, namely to some extent the choice of ordered pair matters. But if you choose reasonably simple encodings then it is likely that you can unpack one to translate to the other but you may have to use the axiom of foundation.
 
4:13 AM
hmm
1
Q: Where is $\Bbb R$ in the von Neumann hierarchy and the constructible hierarchy?

Kenny LauDefinitions $(a,b) := \{\{a\},\{a,b\}\}$ $\Bbb N := \{n \in \infty \mid \forall A (0 \in A \land \forall n (n \in A \to n \cup \{n\} \in A) \to n \in A) \}$, where $\infty$ is the set guaranteed to exist by the axiom of infinity. $\Bbb Z := \Bbb N \times \Bbb N / \sim$ where $(a,b) \sim (c,d) \...

@user21820 would you have any comments?
 
@LeakyNun I'll read it.
No wonder you asked about ordered pairs.
 
well that's a separate question lol
also would you like to explain the two things linked in the answer?
 
But it does matter, doesn't it? If your choice of ordered pair <a,b> was {{{a}},{{a,b}}}, your constructed set of reals would be a few levels higher up in the von Neumann hierarchy.
 
well
 
I am not familiar with the condensation lemma, but it does not look too hard, so let me think about it.
Not now though, since I don't know how long it would take.
 
4:24 AM
ok
 
Intuitively, every definable real is definable by some countable formula and hence would show up once you iterative Godel's L uncountably many levels.
You have a monotonic process that may add a new real at each stage. If it never stops adding reals, then the countably many definable reals must be exhausted at some stage before ω[1].
So it must stop somewhere before ω[1].
If you can make that into a rigorous proof yourself, then I'm saved the trouble. =D
I can't guarantee my intuition is right though, since I haven't looked at the details.
 
4:46 AM
0
Q: Is ZFC under two different encodings of ordered pairs equivalent?

Kenny LauLet $\mathbf{ZFC}$ denote the theory of ZFC. Let $\mathbf{ZF-R}$ denote the theory of ZF without replacement. The motivation is that the remaining axioms do not require ordered pairs. Let $p(x,y,z)$ be a valid encoding for ordered pairs, where $p$ is a formula over the language of ZFC with $x...

@user21820
 
Hello @user21820. I went through the transcript for proof of semantic completeness, and I understood it. Is there anything else you have covered till now?
 
@bat_of_doom No, because we've essentially started from scratch (no logic background).
 
Also, when does today's class start?
 
But you might like to browse some other stuff we discussed, such as the general undecidability theorem here:
2 days ago, by user21820
@mercio: LeakyNun is right that my post does not address his version, so I'll present a short proof of the general undecidability theorem now.
@bat_of_doom There is no formal class. It just so happened that the three of us were in the same room at the same time and they wanted to learn logic. At first I had recommended them to read forallx, but then the mixture of old style arguments (premises, conclusions) ended up confusing so I told them to just ignore the whole thing and I would explain it myself haha..
 
In computability theory, the Turing jump or Turing jump operator, named for Alan Turing, is an operation that assigns to each decision problem X a successively harder decision problem X ′ with the property that X ′ is not decidable by an oracle machine with an oracle for X. The operator is called a jump operator because it increases the Turing degree of the problem X. That is, the problem X ′ is not Turing reducible to X. Post's theorem establishes a relationship between the Turing jump operator and the arithmetical hierarchy of sets of natural numbers. Informally, given a problem, the Turing jump...
@user21820 what is the turing jump?
 
4:53 AM
@LeakyNun Um, it's just the halting oracle? Given a set X, we define X' to be a set that encodes the halting oracle for programs that can use membership in X as an oracle.
 
in English?
 
Lol you know what are programs. Now given any set X of naturals, you can imagine programs that are allowed to call "∈X" at any point. Now the halting problem for those programs cannot be solved by themselves, but the answers can be encoded in yet another set, which we call X'.
Does it make sense? Actually I thought the Wikipedia definition was clear enough, and you like symbolic definitions, right? =P
 
Hi @user21820
let's continue once you are done with @Leaky
 
@LeakyNun: At least the finite jumps should be easy to understand. The first jump is just the halting oracle, which is equivalent to having some particular set of naturals defined by one unbounded existential quantifier. The second jump corresponds to 2. The k-th corresponds to k unbounded quantifiers. In general, you can convince yourself easily that using the k-th jump you can determine the truth value of any arithmetical sentence that has at most k unbounded quantifiers (in normal form).
 
@user21820 for example?
 
5:03 AM
Programs that can use {} are your ordinary programs.
{}' is the first jump of {}, which you can think of as just the ordinary halting oracle, because you can use membership in it to decide the halting problem for ordinary programs.
 
@Secret you are herewith summoned!
 
@LastIronStar: I have to go in a while, and won't be back until a couple of hours later.
 
@user21820 interesting
I may get it
 
@user21820 me too. I am free for say 20 mins
 
@LeakyNun So, for example, if you look at the nice theory ACA that I always talk about, it is more or less saying that we can construct any set that can be decided using some finite Turing jump, and that we also have the full induction schema.
 
5:06 AM
something to read if you don't think thats enough time
 
@LastIronStar Hmm let me see...
@LastIronStar @Secret: I could give you homework hahaha..
Prove the following theorem in the Fitch-system:
7
Q: Intuitionistic logic plus $A → B \lor C \vdash ( A → B ) \lor ( A → C )$

user21820The following is a classically valid deduction for any propositions $A,B,C$. $\def\imp{\rightarrow}$ $A \imp B \lor C \vdash ( A \imp B ) \lor ( A \imp C )$. But I'm quite sure it isn't intuitionistically valid, although I don't know how to prove it, which is my first question. If my conje...

 
@user21820 LOL. If that's what you wanna call it
 
Ignore the part about intuitionistic logic. Just prove that ( A implies B or C ) implies ( A implies B ) or ( A implies C ).
 
what's a ⊢?
 
Ignore that. That question was where I first learnt (from Hanno) about semantics for intuitionistic logic.
 
5:10 AM
@user21820 and me from you :)
 
It's just a curiosity that you cannot prove this classical tautology in intuitionistic logic, and yet adding it as an axiom to intuitionistic logic does not produce classical logic.
 
is it?
 
@user21820 I see
 
@LeakyNun That's what that post was about. You forgot. =P
 
@user21820 interesting
 
5:13 AM
@Timothy: I hate the chat feature here. There should be a room for set theory and logic. Try asking there, maybe someone can help you. — Asaf Karagila Dec 11 at 21:43
lol
Meanwhile still reading the transcript to catch up what you guys are up to before lastironstar's ping of me
 
@Secret That was a week ago, so it still does not explain his words in here. Never mind.
Anyway I got to go. See you all later!
 
@Secret hi!
 
5:32 AM
2
Q: Are there any uncountable sets that are computable?

Dawid KA set $Y\subseteq X$ is computable iff its characteristic function $f_Y:X\rightarrow\{0,1\}$ defined as $$f_Y(x)=\begin{cases} 1, & x\in Y \\ 0, & x\notin Y \end{cases}$$ is computable. In principle $Y$ need not be a subset of $\mathbb N$, it may be e.g. a subset of the Baire space $\mathbb N^{\o...

there are none, which means don't expect to solve problems related to $\pi$ and $e^e$ directly
 
@Secret sure
 
 
4 hours later…
9:14 AM
@LeakyNun: It seems that Asaf had the same kind of argument as I did in mind:
You don't need fine structure and gaps to see no countable step catches all the reals. It's a simple cardinality argument! — Asaf Karagila 1 hour ago
 
 
4 hours later…
12:58 PM
@user21820 a hat!
 
1:48 PM
@LeakyNun: Well might as well put it on before it disappears.
 
@user21820 what would happen if P=NP?
 
P = 0 or N = 1.
 
@user21820 LOL
 
I mean, I must live up to my hat.
Its description is "Just jesting".
 
I think I fell in love today
with projective geometry
 
1:58 PM
Har har.. it's really nice. Have you proven Desargue's theorem purely axiomatically yet?
 
on other news:
0
Q: how can i proved that polynomial ring Z[x] is not an integeral domain?

Michaelhow can i proved that polynomial ring Z[x] is not an integeral domain ? i was thinking that Z[x] is not a field so it is will not form integral domain as every finite integral domain is a fied but here Z[x] contain infinitely many element so ,,it will not form field ..... Is my thinking i...

> i was thinking that Z[x] is not a field so it is will not form integral domain as every finite integral domain is a fied but here Z[x] contain infinitely many element so ,,it will not form field ..... Is my thinking is correct or not pliz tell and verifeid me ?
theorem: finite ∧ integral domain -> field
theorem : field -> integral domain
 
@LeakyNun I downvoted because people should learn basic logic before attempting anything like abstract algebra.
 
guy : infinite -> not field -> not integral domain
me : ?????
 
That's 20% of the downvote.
 
what's the other 80%?
best logic ever
 
2:00 PM
The next 60% is the grammar and spelling.
The last 20% is just holiday discount.
 
rip logic Euclid-2017
Euclid and Socrates and Plato are all rising from their graves
theorem: finite ∧ integral domain -> field; theorem : field -> integral domain; you : infinite -> not field -> not integral domain; me : ????? best logic ever rip logic 0-2017 — Kenny Lau 23 secs ago
 
Actually, I've seen much worse.
 
@user21820 tell me
 
@amWhy: Help us to clear above-mentioned junk! Thanks! =)
You too, if you don't mind.
Anyway, more seriously, if P = NP then the polynomial hierarchy collapses completely. Hardly anyone believes it even collapses to a finite level.
 
rip "P = 0 or N = 1" 2017-2017
what if P is 2 and N is 4 and we are in Z/6Z
 
2:11 PM
So are you helping with the junk? Too few of us otherwise, I think.
 
don't feel like it
how long would it take you to prove that $\omega+\omega$ is a set?
half an hour?
 
@LeakyNun It's obviously a set. Using replacement.
 
@user21820 yes, but writing down the formula takes you half an hour :)
 
That's why you don't write down the formula.
Instead you use definitorial expansion all the way.
 
definition doesn't prove existence
 
2:19 PM
So you need to read my post again:
6
A: How could we formalize the introduction of new notation?

user21820What you may be looking for in your formal system is variously called full abbreviation power or definitorial expansion. Basically, it comprises rules that allows you to create on the fly new symbols extending the original language. We need one type of rule for each kind of symbol: $\def\eq{\left...

 
so you need to prove the prerequisites
0
A: How can I prove that polynomial ring $\mathbb{Z}[x]$ is not an integral domain?

Kenny LauThe only way to prove that $\Bbb Z[X]$ is not an integral domain is to prove that ZFC is inconsistent, because (in ZFC) $\Bbb Z[X]$ is actually an integral domain: Let $f,g \in \Bbb Z[X]$ with $fg=0$. Convince yourself (prove via induction) that if the leading coefficient of $f$ is $m$ and th...

I'm proud of my opening
without the algebra crap
 
@LeakyNun Your answer is wrong. It may be possible to prove ZFC inconsistent without being able to prove that Z[x] is not an integral domain.
 
@user21820 why?
 
⬜false does not entail false.
 
...
I'm not doing modal logic here
I'm actually proving false inside ZFC
 
2:28 PM
You're wrong.
This has nothing to do with modal logic.
 
I mean provability logic
I'm not constructing ZFC inside ZFC
 
You essentially claim that if you can prove ¬Con(ZFC) then you can prove 0=1.
That is invalid.
 
I mean prove it outside
 
That's not going to help.
Proving that something is inconsistent is not the same as actually writing down a proof of inconsistency.
 
ugh
alright
edited
 
2:33 PM
Okay.
 
@user21820 wait, isn't that soundness?
 
Soundness does imply it. But you don't know whether ZFC is sound or not.
 
isn't it an S1 claim inside w?
isn't the proof a natural number?
 
So what? You have no clue whether ZFC is sound or not. Suppose L is some large cardinal hypothesis (an existence claim) that actually implies not Con(ZFC) over ZFC.
Let Z = ZFC+L. Then Z |− not Con(Z).
But Z could very be still consistent.
 
hmm
:o
wait
not Con (Z) is still S1
what is the natural number that proves falsum?
 
2:46 PM
I don't get your question.
Just because a theory proves an arithmetical sentence does not imply that that sentence is true about the natural numbers.
 
Z |- not Con(Z), i.e. Z |- exists x, x proves 0=1
@user21820 but it proves it...
 
I think you forgot what we went through last time. The incompleteness theorems clearly show that if S is nice and consistent then S+¬Con(S) is consistent but Σ1-unsound.
It proves a false Σ1-sentence.
 
but
it proves that there exists such a number
how can it not exist :O
lol
 
Why is it so unusual? S+¬Con(S) cannot be inconsistent, otherwise it proves false and hence S itself proves Con(S).
 
or i'm just jesting
 
2:51 PM
It is easy for a theory to prove false things about natural numbers.
 
come on
 
It is hard to get one that proves only true arithmetical sentences.
 
@user21820 it's impossible
 
@LeakyNun Are you still jesting? Unless you mean that PA− does not.
I didn't say "all and only", in case that's what you're thinking.
 
alright
 
3:06 PM
I'm not sure that $ZFC^p$ is well-defined. One of the favored definitions of $(x,y)=z$ is $z=\{x,\{x,y\}\}$ but this is an abbreviation for $\forall a\;(a\in z\iff (a=x\lor (\forall b\; (b\in a\iff (b=x\lor b=y)))).$ If you want to replace such a string of characters in $\varphi$ with $p(x,y,z),$ there can be a sentence $S$ that is logically equivalent to $\varphi$ but in which parts of this string appear non-consecutively. E.g. somewhere in $S$ it says $a\in z,$ elsewhere in $S$ it says $\{a,b\} \in z$ and elsewhere in $S$ it is asserted that $z$ has at most $2$ members. — DanielWainfleet 8 hours ago
@user21820 what does this mean?
 
@LeakyNun I read that comment and also did not know what it meant, so I didn't bother wasting time trying to figure out.
 
:o
 
But you could ask him to clarify.
In any case, assuming Asaf and Noah are correct, the only possible issue you could have is in proving that you in the first place have a definable pairing function with definable projection functions.
Which is why earlier on what I stated had to do with that.
You can see this clearly from (again) definitorial expansion. Because once those are definable you can add them to the language and use them with their defining properties. You can also prove (as meta-theorem) that any such pair coding can be provably translated to any other, which is easy using those newly defined symbols. So each axiom using one would imply the same axiom using the other.
 
 
2 hours later…
4:48 PM
@LeakyNun: Interesting; I just learnt something very simple that I somehow didn't realize from this comment:
Thank you! But i'm still somewhat confused: I don't think that Con(T) implies Con(T + Con(T)), otherwise the theory T + Con(T) could prove it's own consistency. So one cannot take Con(ZF + V=L) as an example for a statement provably independent of ZF + V=L. Or am i missing something? — user4607 Mar 13 '10 at 18:20
In this general case, one must use the Rosser sentence. The issue you mention is exactly the difference between the Goedel Incompleteness theorem and the Goedel-Rosser Incompleteness theorem. The statement sigma you want is: "For any proof of me, there is a shorter proof of my negation". — Joel David Hamkins Mar 13 '10 at 18:41
In particular, if S is nice and consistent then S |− Con(S)⇒Con(S+Ross(S)).
But it cannot be that S |− Con(S)⇒Con(S+Con(S)), otherwise S+Con(S) |− Con(S+Con(S)) contradicting the incompleteness theorems.
In computability terms, S can prove a formalization of the incompleteness theorem in my post, where Ross(S) is replaced by the appropriate statement of the halting of some program on itself.
Here "nice" includes "interprets PA" since we need enough induction to formalize the proof.
 
hmm
 

« first day (490 days earlier)      last day (2344 days later) »