Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 29 of 29
Hi Marc, welcome to the nForum!
this looks by a quick glance interesting. Without reading it (and so I can’t really comment), may I make a suggestion which you are free to ignore: use locales instead of topological spaces (or else use simplicial objects). This requires less strength in $(L,A,r)$. Also, to make things interesting, consider having excluded middle as a hypothesis, not a background assumption. This opens up the possibilities that 1) it could be removed or 2) it is essential, and therefore gives interesting examples where this result fails.
Hi Marc! The idea of proving the Incompleteness theorem with group actions and topology is interesting. I haven’t thought in detail about your proposal. But it’s not clear to me that this outline is essentially different from the usual proof; it seems to me that the process of formalizing your statements NFP, Q, and R inside the given theory will be essentally the same as the way that logic is coded up more explicitly in the usual proof. But perhaps I am misunderstanding?
a monoidal action of Non-negative integers by applying NOT n times
In intuitionistic logic, it’s a little simpler than this, since $\neg\neg\neg{p} = \neg{p}$ still. So it’s an action of the $3$-element monoid of nonnegative integers modulo the relation $3 = 1$.
@Marc - I guess Mike could have pointed out as a warning the so-called topological proof of the infinitude of prime numbers (’so-called’ because it uses a topology, but the actual meat of the proof is still one of the classical ones, rewritten in terms of the topology).
@Toby - I was going to say something similar. We have also $\neg\neg\neg\neg{p} = \neg\neg{p}$ - the double negation operator is an idempotent, but there is more structure, as you point out.
@Marc - yes. In fact, it can’t be anything else.
R is essentially the statement “Q is not provable in system A”. Your theorem is “If A is consistent (and furthermore sound), then either Q is not provable in system A or Q is true”. The parenthetical is because, in proving your theorem, you invoke the soundness of system A. But then there’s hardly anything to this theorem; it does not seem like Goedel’s incompleteness theorem. It seems like just recalling the very definition of soundness.
What would be more like Goedel’s (2nd) incompleteness theorem (since Q is essentially the statement “A does not prove its own consistency”) would be a theorem of the form “If A is consistent, then Q is true”, with both a weaker assumption and a stronger conclusion. But you haven’t really sketched out how to prove this stronger statement, and it’s not clear to me yet how anything would be gained from the topological formulation in doing so.
Regardless of whether the system is sound, if LEM applies, then either it can’t prove X or it CAN prove X, for any X. I don’t see why you would call this incompleteness; incompleteness normally means that (if the system is consistent/sound, then) the system both can’t prove X and can’t prove NOT X, for some X. Or, slightly differently, the more primary form of Goedelian incompleteness is that (if the system is consistent, then) X is true and the system cannot prove X, for some X.
Put another way, let’s look at your description “incomplete in a way that either it can’t prove its consistency or it can’t prove that it cant prove its consistency”. This applies even to the (not effectively axiomatized, purely ideal) theory comprising all and only the true sentences of arithmetic/topology/whatever! That is, suppose you had a theory which both could prove its consistency, but couldn’t prove (the therefore false statement that) it can’t prove its consistency. Why would this be considered a form of incompleteness? I see no reason why it should be, but you seem to be doing so.
There are a number of things I want to address. First is that $\neg$ acts contravariantly, not covariantly. In other words, if $P$ is a Heyting algebra (whose elements $p$ we’ll think of as propositions or predicates), then $\neg$ is a functor $P^{op} \to P$, not a functor $P \to P$. So the statement that there is an induced continuous function $|\neg|: |P| \to |P|$ should be clarified. It is indeed true that for any category $C$, there is a canonical homeomorphism $|C| \cong |C^{op}|$, ultimately due to the fact that the unit interval is interval-homeomorphic to the “opposite” topological interval (i.e., with reverse ordering), via $t \mapsto 1-t$. So what we get is a composite
$|P| \cong |P^{op}| \stackrel{|\neg|}{\to} |P|$but it’s not at all clear to me what consequences fixed points of this hybrid (i.e., this mix of logic and $t \mapsto 1-t$ stuff) would have for logic.
Next, in intuitionistic logic, if $\neg^n = 1$ for any $n$, then $\neg^2 = 1$. For we have $p \leq \neg \neg p$ for any (predicate) $p$, and since $\neg$ is contravariant, we have also $\neg \neg \neg p \leq \neg p$. From these two facts, we conclude $\neg p = \neg \neg \neg p$ for all $p$, as someone said earlier. Now if $\neg$ were a bijection (as would follow from any equation of the form $\neg^n = 1$), we conclude from that last equation that $p = \neg \neg p$ for all $p$, or that $\neg^2 = 1$. It follows in particular that $n$ cannot be odd, else we reach the absurdity $\neg = 1$.
Actually, maybe I’m not understanding this $\neg$ to begin with. Is it supposed to mean the negation operator on a Heyting algebra, or is it something more modal like “not provable in a formal system”, or, …?
Some of the ideas outlined above look interesting to me, and most of the earlier replies have viewed the outline on a somewhat broader distance scale. This comment could be said to have to do with up-close details.
Well, a fixed point of that hybrid is still a proposition $p$ such that $p = \neg p$. Intuitionistically, a fixed point of that hybrid still amounts to the same thing as the presence of a contradiction (i.e., that hybrid has a fixed point if and only if $P$ is the one-element Heyting algebra). The contravariance of $\neg$ doesn’t seem to me a problem for the use being made of its fixed points, but perhaps I am misunderstanding the issue which concerns you. [On edit: Oh, I see, on the topological account, there may be fixed points which are not actual propositions (and thus are of unclear significance); there could be a fixed point living somewhere in the middle of an arrow connecting two propositions. Is that the concern?]
(As someone else responding to details, I am still concerned that I don’t see anything in the original argument with NFP, Q, and R that has anything to do with “incompleteness”. [E.g., an argument that $P$ could not be the two-element Heyting algebra])
there may be fixed points which are not actual propositions (and thus are of unclear significance); there could be a fixed point living somewhere in the middle of an arrow connecting two propositions. Is that the concern?
Well, yeah. Let’s take maybe the easiest possible example: the negation on the Boolean algebra $2 = \{0 \leq 1\}$, where $\neg: 2^{op} \to 2$ is an isomorphism. The geometric realization is the unit interval $I$, and the corresponding map is $t \mapsto 1-t$. There’s a fixed point at $t = 1/2$. And so?
To make matters slightly worse, I said there was a “canonical” order-reversing homeomorphism $I \to I$ which is used to exhibit $|C| \cong |C^{op}|$, but I lied. There is nothing, as far as I can tell, that makes the order-reversing homeomorphism $t \mapsto 1-t$ (as used on the page I referred to) particularly canonical, and therefore I don’t see a “canonical” homeomorphism $|C| \cong |C^{op}|$. So the fixed point $t = 1/2$ above isn’t particularly meaningful to me.
You’re right that fixed points of the underlying function $\neg: P \to P$ transfer to fixed points under $|P| \to |P|$, but that doesn’t account for all of them.
Right, right, I understand you now. In fact, we’re guaranteed fixed points in the topological setting, regardless of consistency or completeness, because, as you note, we will always have an arrow from False to True which negates into itself (and every continuous map from the unit interval to itself has a fixed point).
Although I am also confused as to what exactly is being done in the topological setting: are we losing information about the directedness of arrows by regarding $C$ topologically? Or are we meant to be working with some notion of directed topological spaces? If we’re going to be generalizing in this fashion, why not just work directly with the concept of categories/preorders and thus not have to worry about the idea of fixed points “within” arrows? [Full disclosure: My (slowly being written…) thesis work is on a category-theoretic account of the Goedel-Loeb modal logic of provability (including the “incompleteness” phenomena) and associated fixed point theorems]
There must be some degree to which a fairly wide variety of categories arise from logical systems.
Certainly! There is a lot of material out there on this; the phrase “propositions as types” refers to a sort of paradigm where structured categories (not just structured posets) correspond to various parts or fragments of logic.
One basic instance of this is cartesian closed categories, seen as categorical generalizations of Heyting algebras. I’m not good at making tables, but we have basically a series of analogies
Heyting algebra: cartesian closed category
meet $a \wedge b$: cartesian product $A \times B$
implication $a \Rightarrow b$: exponentials/internal homs $B^A$
join $a \vee b$: coproduct $A + B$ (we’ll assume our cartesian closed category has coproducts, okay?)
so that a Heyting algebra, which is the algebraic concept corresponding to intuitionistic propositional logic (as Boolean algebra corresponds to clasical propositional logic), is just the posetal special case of a cartesian closed category. We can go on and interpret formal deductions in intuitionistic propositional logic as morphisms in cartesian closed categories: there is a formal semantics for doing this.
People around here could talk about this stuff all day long…
There are well known wikipedia documented facts that the image of geometric realization is better characterized as CGH.
Hey, you’re at the nLab, where the facts are even better documented. :-) For example, check out what we have over at geometric realization (and related articles), and convenient category of topological spaces (and related articles). When you see the phrase “convenient category of spaces” around here, that’s code for a cartesian closed category of spaces (like CGH) having other nice properties, and people here are very familiar with the technical convenience of such things.
Speaking of logic and topological spaces, there’s another big area of study under the general rubric of “domain theory”. I don’t think we have too much on that yet here at the Lab, but there one finds aspects of computation modeled by suitable spaces and continuous functions, so it’s something you’d probably be interested in.
I’m not good at making tables,
It’s at types and logic - table.
1 to 29 of 29