Logic - 2019-01-29

« first day (895 days earlier) ← previous day next day → last day (2217 days later) »

famesyasd

00:15

@user21820 How do you determine if "forall x : S φ(x) : bool"?
I thought of "forall x : S (φ(x) : bool) ⊢ forall x : S φ(x) : bool" and same for "exists"

I mean

or maybe it should be "forall x in S (φ(x) : bool) ⊢ forall x : S φ(x) : bool"

Does the notation forall x : S exists y : T phi(x,y) make sense? Did it begin being meaningful after those two rules you have added?
Q(E) ⊢ E : { x : Q(x) }.
E : { x : Q(x) } ⊢ Q(E).
if yes, (I guess with them I can now quantify on types) then how were you supposed to check whether or not you can use lem on "forall x φ(x) or not forall x φ(x)" before them

1 hour later…

famesyasd

01:38

also there should be a rule that if x[1..n] : S[1..n] ⊢ P(x[1..n]) : bool

where P is some predicate symbol

famesyasd

01:49

I can't write "forall x x = x" now lol!

famesyasd

02:05

ah no, I can

famesyasd

02:21

to prove forall A,B,C if A ⊆ B, B ⊆ C then A ⊆ C does not require any axioms of set theory, does that mean that this is such a fundamental fact about sets or something?

famesyasd

03:17

@user21820 do we have a rule that "x : S ⊢ x : obj"?

user21820

04:11

@famesyasd A lot of these decisions must be made together as a whole. In our current discussion, I'm assuming we have the logic part of my system. Many decisions have to be made simultaneously when we go beyond that.

For example, if we replace the syntactic rules by the typing rules as above, and we have a type of all sets, then we construct a predicate-symbol R := ( set x ↦ x∉x ). From now on I'm going to use "ref(S,T)" instead of "func(S,T)" for the type of function-symbols with input in S and output in T. As before, we would add the axioms "R : ref(set,bool)" and "∀x∈set ( R(x) ⇔ x∉x )", and we have the axiom "R : ref(set,bool) ; x : set ⊢ R(x) : bool".

The question is, can we also have "R : obj"?

The answer is, as always, it depends on what else we want to have. We certainly cannot also have the rule "S : ref(set,bool) ⊢ S : set ; ( x : set ⊢ x∈S ⇔ S(x) )", otherwise we get "R : set" and hence "R(R) ⇔ ¬R(R)".

But if you don't add this kind of assumption that every object must be captured by a set, then I think that rule is safe, even with the axioms and rules given under "Set Theory" in my system. The reason I cannot be 100% sure is that my rules allow you to construct any explicit set of objects, so if R is an object then you can construct {R}. What would that mean? Well, R is simply a syntactic object, so {R} would just be the set whose only member is that syntactic object. I don't see any problem.

@famesyasd ∀x∈obj ( x = x )".

@famesyasd Yes you do the same thing with predicate-symbols as with function-symbols. Since it's just a matter of changing "T" to "bool", I didn't bother stating it yesterday.

@famesyasd Yes indeed I didn't include all the typing rules yesterday, so it's good that you can figure them out yourself, such as for equality and now quantifiers.

Same for "∃".

@famesyasd Using the typing rule you have figured out, you would need to prove "Given x∈S ⊢ ( Given y∈S ⊢ φ(x,y) : bool )", and then you can prove "Given x∈S ⊢ ( ∃y∈S ( φ(x,y) ) : bool )" and hence "∀x∈S ( ∃y∈S ( φ(x,y) ) ) : bool".

famesyasd

04:44

what

no it would be wrong to deduce that

user21820

What is "that"?

famesyasd

"Given x∈S ⊢ ( Given y∈S ⊢ φ(x,y) : bool )"

it's wrong

no?

user21820

What's wrong? I'm saying you need to have already proven that before the rest works.

famesyasd

ah I see

user21820

For example, we can prove "Given x∈S ⊢ ( Given y∈S ⊢ x=y : bool )", and hence "∀x∈S ( ∃y∈S ( x=y ) ) : bool".

famesyasd

04:49

yep

user21820

I'll also note that in practical implementation of this system, all typing inferences can be done deterministically (and hence automatically) by the proof assistant, so the user will not have to supply any statement of the form "x : S".

Taking the above example, if you create a subcontext "If ∀x∈S ( ∃y∈S ( x=y ) ):", the proof assistant knows that you are only allowed to do that if you prove "∀x∈S ( ∃y∈S ( x=y ) ) : bool", so it can automatically check (reversing the above process) whether you can get "Given x∈S ⊢ ( Given y∈S ⊢ x=y : bool )", and at that point it sees that it's correct because of the typing rule for equality.

So in fact, the user does no more work in using such an implementation than in standard FOL, and yet has the benefit of type-checking!

@famesyasd Yes it works for any types A,B,C, where "S⊆T" is short-hand for "∀x∈S ( x∈T )".

Set theories should be thought of as systems that govern certain special kinds of types. For all we know, ZFC could be inconsistent or unsound or meaningless. In contrast, the fact you mentioned is more a fact about subtyping than anything to do with any kind of sets. You could even extend "⊆" as follows:

"S⊆T" means "x : S ⊢ x : T".

Then it is obvious that if S⊆T and T⊆U then S⊆U.

Does this make sense? Thinking in terms of types can be very illuminating in my opinion.

(Away for a while.)

famesyasd

@user21820 Do you mean I can construct nonsets with your rules (that is, types)? I missed how I can do that.

I only used types for type-checking that's all

@user21820 nope :) I mean this fact follows straight from logic but you can interpret it in terms of sets or how you did in terms of types even. Does that make it some special fundamental truth about types/subtypes just because we found some interpretation or does it still has nthing to do with them simply because we derived it only from logic, without using any connections from type theory

user21820

05:23

@famesyasd Well yes it follows straight from logic, if you already have the binary relation-symbol "∈". The point is that it's in some sense true even if you don't, because it applies to any pre-existing or definable types in the sense we've been using them.

@famesyasd Look for the "type-notation" rule. In standard set theory the types constructible via this rule would be called classes.

famesyasd

@user21820 ? no such rule there or at least you haven't called it by the name

user21820

@famesyasd Under "Set Theory" in my post.

famesyasd

right but we only have E:{x:P(x)}⇔P(E)

not E∈{x:P(x)}⇔P(E)

user21820

@famesyasd This isn't what I wrote there...

famesyasd

where?

user21820

05:32

In the post. I know I used "∈" in that post for type membership as well as set membership, because in standard set theory every type has boolean membership.

But it's syntactically invalid to write "E:{x:P(x)}⇔P(E)".

Over here, I gave the weaker version:

Q(E) ⊢ E : { x : Q(x) }.
E : { x : Q(x) } ⊢ Q(E).

famesyasd

what's the difference

user21820

It's actually as powerful, because of what I wrote next.

If we permit forming types that don't even have boolean membership, then the one I gave here is the right one.

In standard set theory, every class has boolean membership, so both give the same results.

famesyasd

okay I

I

I'm confused

user21820

Firstly, both versions require you to have proven "x : obj ⊢ Q(x) : bool".

The version in my post then allows you to prove "E∈{x:Q(x)}⇔Q(E)" if you have "E : obj".

The version I gave here only allows you to prove any of "E∈{x:Q(x)}" or "Q(E)" from the other.

Both versions are equivalent because of the requirement.

You can ignore what I said about non-boolean type membership if that's confusing now.

Anyway, you must remember that ":" is not a binary-relation-symbol, so you cannot use it as if it is. It's more accurate to think of it as a meta-level notation.

famesyasd

wait, so it's "E∈{x:Q(x)}" now?

@user21820 here there's no "in"

user21820

05:46

Sorry, as I said I used "∈" for both type membership and set membership in my post. That's why it's confusing when we're joining the two.

In standard set theory, the idea is that some types (classes) are sets. So it was convenient to use the same symbol.

famesyasd

@user21820 so the rules are prove that "x : obj ⊢ Q(x) : bool" then you can use those?

user21820

Yes.

famesyasd

okay

user21820

In general type theories, it's better to keep the meta-level ":" separate from the internal "∈". That's why I used ":" here for typing.

That's also why we needed a rule to elevate sets to types.

In my post you see no such rule because I 'cheated' by using the same symbol. =P

Which is what set theorists do anyway. Do you know MK set theory? It has classes and sets, and both use the same "∈".

famesyasd

nope

okay so in the end with the rules you gave here I only use types for type-checking, correct? no classse nor anything, I don't even understand why would I want to have "in" for types

user21820

05:53

Yes that was the original purpose of the conversation here, to show that we can overlay a type system on top of whatever first-order system you start with, in order to restrict theorems and proofs to meaningful statements.

Only when we want to be able to define new types, would we need something like what I had in my post.

It's important in actual mathematical practice. For example, we want to have a type of all finite graphs, or a type of all well-orderings, or things like that, and then quantify over them in a proof. That last bit cannot be done in an efficient manner without being able to define new types.

For example, you could define a new predicate-symbol FinGraph, but then your theorems would have to look something like "∀G∈obj ( FinGraph(G) ⇒ ... )". Whereas if you can define the type FinGraph, then you can use "∀G∈FinGraph" and reason nicely.

famesyasd

how come all finite graphs do not form a set

user21820

Because if it is then you can extract a set of all sets from it.

famesyasd

graph is a subset of N times N right?

(V,E) subset N times N

so they all lie in P(N times N)

user21820

@famesyasd That's the usual way to cheat in some cases like finite graphs. You can see that cheat and other examples where cheating is impossible here:

1

A: When is a proof or definition formal?

There is one aspect of "definitions" that is not exactly asked in your question, but is relevant to mathematics. There are actually two kinds of completely formal definitions, arising from two separate mechanisms: $ \def\nn{\mathbb{N}} $ Definition by existential instantiation: When we have an ...

Point 2.

famesyasd

@user21820 isn't this essentially NBG?

user21820

06:04

@famesyasd Depends on your type-construction rule. In the one in my post, yes, because we cannot quantify over types when constructing a type.

In MK set theory, one can define a class with a formula that quantifies over all classes. That makes it stronger (and even harder to swallow).

Already in ZFC, one can define a set that quantifies over all sets. I don't know how you feel about that haha..

famesyasd

@user21820 you meant define a set with a formula that quantifies over all sets?

user21820

@famesyasd Yes ZFC can do precisely that! And hence I also permitted that in the system in my post, to make it compatible with current mathematics.

famesyasd

@user21820 to deal with the "lim" notation requires even more type theory?

user21820

@famesyasd You mean like "lim[n→∞] ..."?

famesyasd

yeah

\lim, \sum, \int all those I think they are all similar

user21820

06:18

Well, you just have to set up new inference rules for the new notation. Limits are the most tricky. One issue is to decide how to deal with limits that don't exist. My preference would be to define a predicate-symbol for LimitExistsAt, and then you can define the function-symbol LimitAt for only (function,input) pairs that satisfy LimitExistsAt.

famesyasd

is "\sum_{i=n}^m a_i" also a function symbol that receives (n,m,a) triple?

where a is a function

user21820

Another issue is what kind of functions to support. Ideally, you want to be able to talk about any real function on a subset of the reals. And also, if you have constructed D := { x : x∈real ∧ x>1 }, do you want to be able to write "LimitExistsAt( ( D x ↦ ... ) , −2 )"? Would you consider it meaningful? If so, probably you want it to be false. If not, then you can't even use a predicate-symbol for LimitExistsAt if you want to force the second input to be in the domain of the first input.

@famesyasd Yes that works. And summation won't have as much trouble as limits.

famesyasd

and if the summation is infinite then "\sum_{i=0}^\infty a_i" denotes a function symbol that receives a and outputs a sequence with its members being finite sums of a from 0 to n?

user21820

@famesyasd Infinite summations have to be defined after you define limits, because it's a limit of the partial sums.

famesyasd

haha

that is, if the limit exists

user21820

06:28

Exactly.

That's why limits are the biggest problem to formalize in analysis.

famesyasd

do you see the overload here?

we denote as "\sum_{i=0}^\infty a_i" both the sequence and its limit, if it exists

user21820

@famesyasd No in standard mathematics that never denotes the sequence.

The sequence is a itself.

famesyasd

I'm pretty sure I've seen in 3 books that it was mentioned explicitly that it does denote the sequence formed from partial sums of a

and if the limit of that sequecne exists then the very same notation denotes its limit

user21820

@famesyasd I'm afraid those are not standard; I've never seen any standard text do that, because it doesn't make sense.

We define Sum[k from 0 to ∞] f(k) := lim[n→∞] Sum[k from 0 to n] f(k) and that's it.

famesyasd

and how do you denote the sequence of partial sums then

alright I checked Tao and Rudin

Tao only defines it to be the limit

and Rudin does both

lol

another (Russian) book defines it to be both

Folland defines it to be both

another (very good) Russian book defines it only as limit

user21820

06:47

I'm surprised. Why would anyone want "sum" to mean "sequence of partial sums"?

Lol.

@famesyasd ( nat n ↦ Sum[k from 0 to n] f(k) ).

famesyasd

okay, so this is all one big function symbol?

user21820

Which would be ( N n ↦ Sum(f,0,k) ) after you've defined finite summation.

famesyasd

you meant ( N n ↦ Sum(f,0,n) )

user21820

Yes sorry.

famesyasd

what's this notation?

yeah I guess that's just one big function symbol

@user21820 yeah no, If x is not an adherent point of D then LimitExistsAt should be false

so that we do not consider such points as -2

well anyway when I asked about limits I thought that you would maybe suggest something of this kind

user image

I can't quite transfer what is written there so I can't quite understand did they do something cool or not

ahhhh

user21820

07:03

@famesyasd Oh wait you do want to allow limits to points outside the domain, so you should permit writing "LimitExistsAt( ( D x ↦ ... ) , −2 )", and even proving that it's false.

famesyasd

yeah predicate should be defined everywhere but should be false for -2

user21820

And in the example given you want "LimitExistsAt( ( D x ↦ 1/x ) , 1 )" to be true (and provable).

@famesyasd Yep makes sense.

famesyasd

what does?

user image

here's the second part in case you're wondering

user21820

@famesyasd It makes sense to define RF := { f : ∃D∈set ( D⊆real ∧ f∈func(D,real) ) } and then define LimitExistsAt : ref([RF,real],bool), so that you can ask whether any given function in RF has a limit at any given real.

famesyasd

@user21820 can you decipher what is written on those pictures, do they do something superior to what we are doing or not?

user21820

07:19

They are using a weird definition of canonical error-values.

For any type S the error value of type S is defined as ⊥[S] := Ix : S . x ≠ x, which says "the x in S such that x≠x".

Lol.

famesyasd

you've got the copy?

user21820

I guessed you were reading "seven virtues ..." which is available online.

So their approach is somewhat non-classical, and I would in fact prefer my (3-valued) type theory, where there is just one unique "null" that represents "no output" in exactly the manner we would like.

famesyasd

yeah

so what are they doing with the limit, is it superior in some way because I don't understand those notations at all so I don't get what they are doing

user21820

It's a matter of whether you still want the underlying logic to be standard FOL or not. If you do, then what we've been discussing is in my opinion the best way. Their way requires changing the underlying logic to a truly type-theoretic system, and they will face significant issues with reasoning about types (which is why they even have a section on subtyping to try to remove a small part of the issues).

And the requirement that every object has a type is also why they need an error-value for each type, which I don't like.

Aha see section 8.4 Undefinedness:

> With little difficulty, the semantics of STT can be modified to admit undefined expressions and partial functions. As a result, improper definite and indefinite descriptions would be undefined and error values would no longer be necessary. This extension of the semantics can be achieved by either preserving the classical two-valued nature of simple type theory [17,19] or by extending simple type theory to a three-valued logic [38].

The last bit is exactly what I came up with too.

On looking up the reference [38], I realize that I downloaded it before almost exactly 1 year ago and saved it in my "References" folder. =)

Looking at the paper again, I think that my type theory is better. =D

famesyasd

07:36

xD

user21820

In summary, we have standard FOL, and we can enforce strict typing as we've discussed, let's call that FOL*. We also have non-classical logics like intuitionistic logic I (the basis of CoC used in Coq) and (Kleene's) 3-valued logic (used in that paper) 3VL. If you enforce strict typing on that to get 3VL*, it would be reasonably close to the underlying logic of my type theory.

I should stop using "*", as chat likes to think it represents italics...

STT (simple type theory) is a forerunner of CoC (calculus of constructions).

famesyasd

what's the point of "f : func(S,T) ; x : S ⊢ f(x) : T." rule, isn't f : func(S[1..k],T) ; x[1..k] : S[1..k] ⊢ f(x[1..k]) : T" coming from the new symbol rule already enough?

user21820

Yes I just repeat myself enough times so that nothing goes missing. =)

But remember, don't use "func" for new symbols if you also use "func" for ZFC functions as per the system in my post.

They aren't compatible for the same reason that the type of all sets is not a set.

famesyasd

alright

there's maybe only a couple of things left that I might not udnerstand, I'll work through some theory and ask them later

now I think I'll go to sleep

see you tomorrow

user21820

08:03

Good night!

5 hours later…

user21820

12:34

In general, if we represent computable reals by digit-generating programs or rational approximation programs, there is a program $D$ that, given as input any program $A$ that enumerates a collection of computable reals, will produce as output some computable real not enumerated by $A$. The proof is exactly the same. So for example you can use $D$ to construct a computable real that is not expressible using arithmetic, polynomial-roots, exponentiation, logarithms, trigonometric functions, and whatever other (computable) special functions you wish. — user21820 1 min ago

This is related to the fact that, logically, the diagonalization does not invoke any further quantification in defining the constructed counter-example. So if the given program enumerates a subset of some set S that is closed under computation, then its diagonalization will also be in S.

This also shows, indirectly, that there is no program that enumerates all computable reals. But of course we already know that (via the halting problem), don't we? =)

The original post was about transcendental numbers, but hey, computable reals are fun to play with. =)

user21820

13:25

→ 2 messages moved to Basic Mathematics

Read the room description before posting.

« first day (895 days earlier) ← previous day next day → last day (2217 days later) »

Transcript for

Jan '1929

♦ $Mathematics$ Logic

This room is meant for discussion about logic, including found...

formal-systems foundations logic no-trolls

join this room
about this room

00:00

06:00

12:00

18:00

all times are UTC

site design / logo © 2025 Stack Exchange Inc; legal

mobile