Logic - 2021-09-05

« first day (1845 days earlier) ← previous day next day → last day (1266 days later) »

user76284

02:44

Btw, there's an amazingly concise system from Harvey Friedman that interprets ZFC: math.stackexchange.com/a/4242131/76284

8 hours later…

user21820

10:49

@user76284 Oh no wonder you mentioned mod 2.

user41805

isn't mod 2 also definable in presburger's? Ey, (1-r) + x = 2×y where x is input and r is the residue

@user76284 but i think i remember reading that presburger's + squaring is undecidable

user400188

So I recently learnt about reference and extensions, and I was wondering what the precise definition of them actually was.

I have read that the extension of a name is an object, the extension of a statement is a truth value, and the extension of a predicate in the language was a collection of pairs of truth values for each object (or should it be names?).

However, when I look up extension on wikipedia, they seem to only refer to the names that the predicate is true for. In later parts of the lecture series I learnt them from, they do the same thing. It makes me wonder if I have misunderst…

2 hours later…

user21820

12:47

@user41805 Since you can't use multiplication, you mean "y+y". And you don't mean subtraction either. To claim that it is definable, you would have to prove ∀x ∃!r ∃y ( x = y+y+r ∧ r ≤ 1 ). Indeed, it is possible, though not obvious at first glance. In fact, it takes quite a while to prove it from the axioms stated on wikipedia... At least, my proof is rather long. Do you have a short proof (not meta-proof)?

@user76284: Anyway, there is a short meta-proof. Presburger is a complete theory but a subtheory of PA, and so every true arithmetical sentence involving no multiplication is provable in Presburger. This includes the very sentence I just stated for definability of mod2, by just syntactic observation.

"r ≤ 1" is short for "∃s ( r+s = 1 )".

user41805

@user21820 my bad i didn't think clearly

@user21820 i am unfamiliar with ∃!, does it mean exists only one such r?

user21820

@user41805 Yes, it's the standard uniqueness quantifier, and you know how to express it using plain quantifiers, right?

user41805

i think ∃r P(r) ∧ !∃s,s≠r∧P(s) would work

user21820

@user41805 Yes but you need brackets otherwise "∃r P(r)" would be conventionally treated as one conjunct.

Typically, it's stated in the equivalent form ∃r ( P(r) ∧ ∀s ( P(s) ⇒ s = r ) ), or another equivalent form ∃r ( P(r) ) ∧ ∀r,s ( P(r) ∧ P(s) ⇒ r = s ).

user41805

@user21820 that is what i intended...

user21820

13:00

Then it's wrong.

user41805

oh right, i reuse r later

user21820

Yup.

user41805

got it now thanks

user21820

@user41805: By the way, the reason we have this condition for definability, and in general as described here:

A: How could we formalize the introduction of new notation?

What 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...

Is because definable predicate/function-symbols can literally be added to the language with suitable axioms and then used as if it is part of the language.

That makes it very much easier to reason about a theory, because we can add definable symbols to make our life much easier.

You need a meta-proof that the proofs you can do over the expanded theory can be translated to proofs over the original theory, and for that meta-theorem you can either prove it yourself or check the Rautenberg reference I gave in a comment.

user21820

13:56

@user400188 Most philosophy writings on "extension" or "extensionality" are extremely unclear. On the other hand, there is no precise mathematical definition of that notion either, because once anyone formalizes it in some foundational system then one is unable to talk about that same notion in other systems that are too different. So you'd have to make do with my not 100% precise intuitive explanation:

A string of symbols has no meaning in itself; you have to use some interpretation before it becomes meaningful. In a formal system, an expression can refer to an object (via the intended interpretation of the system). Of course, multiple expressions may refer to the same object. The extension of an expression is its meaning. So arguably there's no difference between "reference" and "extension".

But when applied to various concepts, many people start to get lazy and just tell you what the final outcome is. Under an interpretation, every expression (including a constant-symbol) refers to some object, so they say (slightly misleadingly) that the extension of that symbol is an object. Why slightly misleading? The term "extension" only makes sense under an interpretation, but of course people are lazy to say "under the intended interpretation".

Even more misleading is when they say the extension of a statement is a truth-value. If you think of boolean truth-values as objects, then yes under the intended interpretation of a classical FOL system every statement refers to some boolean. But that is not the conventional approach, because booleans are not in the domain of the intended interpretation! The quantifiers in one-sorted FOL range over the domain but not booleans!

So only if you think of booleans as objects (especially in a many-sorted FOL), then it makes perfect sense to say that every statement in classical FOL refers to a boolean, and hence has a boolean extension.

The worst is when they say the extension of a predicate is the collection of pairs encoding the mapping from inputs to truth-values given by that predicate. In the first place, a predicate is not an object expression, so what should it refer to? This is where people prefer the term "extension" because it doesn't "refer" to any object. You can define its extension (under a given interpretation) to be a function that maps each input tuple to its (boolean) value.

That suffices because it pinpoints its meaning under that interpretation. And it should be no surprise that the term interpretation itself must include such a function for each predicate-symbol! (Similarly for function-symbols.)

But some people don't like functions to Bool, or they have always been taught to encode a predicate-symbol's interpretation as a set. And they can. You just need to know the set of all input-tuples that are mapped to true. It suffices just as well as the above alternative.

The first source you are referring to takes the first approach (they prefer to think of the extension of a predicate as a set of mappings, just like when you interpret a function-symbol). Wikipedia takes the second approach (also common in logic texts).

Both are fine, because "extension" never had a precise definition in the first place. You just need to know what precisely they are talking about when it comes to the actual mathematics.

@user400188 Note that your rephrasing of wikipedia's version is incorrect because the extension is not any kind of set of just "names". It must, as I said above, be tied to an interpretation, which comes with a domain, and the extension of a predicate can be defined as the set of all input-tuples of objects in that domain that satisfy the predicate. Nowhere does it mention "names" (or constant-symbols), because that is wrong.

4 hours later…

user76284

18:25

What do you think of Harvey Friedman's 2-schema system? I was elated when I learned of it. For a long time, I've had a feeling that Replacement, Powerset, Union, Infinity, etc. should be derivable from some deeper, more fundamental principle. Page 7 onwards of the second paper has an amazing philosophical explanation of the RED schema. It also shows minor tweaks of these simple schemas yield large cardinals!

I wonder if they can be simplified even further... perhaps even into a single conceptually-atomic schema.

« first day (1845 days earlier) ← previous day next day → last day (1266 days later) »

all rooms