Logic - 2018-03-05

user21820

07:07

@MatheinBoulomenos @skullpatrol @LeakyNun: Hey I found a gem today:

> I'm not certain whether I agree with the statement "However, when we use an axiom in a proof, we normally know whether it holds for standard integers or not." For example, ZFC proves the consistency of theories which I'm not fully confident are consistent, so I'm not fully confident in ZFC's consistency, let alone its arithmetical soundness. But the ZFC axioms are of course widely used (including by me!).

> So I'm not sure that we are always justified in our confidence in the arithmetical soundness of the axioms we use. – Noah Schweber 3 hours ago

Lol.

user21820

08:25

@LeakyNun @MatheinBoulomenos @skullpatrol: I decided to post an answer, which sums up some of my views, including a mathematical explanation of the potential danger of unfathomably deep inconsistency:

0

A: How can we know we're not accidentally talking about non-standard integers?

We know that any formal system cannot completely pin down the natural numbers. Incidentally, I said exactly this here. Besides what I said in that post, I wish to elaborate on the following points: A generalized version of the Godel-Rosser incompleteness theorem shows convincingly that the...

Leaky Nun

09:37

eh, so what is the verdict

user21820

09:52

@LeakyNun Verdict on what point?

On ZFC?

Or on mathematics in general?

@LeakyNun?

Leaky Nun

10:09

maths in general I guess

user21820

@LeakyNun Well, for ZFC I am confident that it is actually consistent, not because it has a model, but because of syntactic reasons, but I don't know enough to explain or justify my intuition about this. However, I am not confident that it is sound, though I do not have any idea what is the level of the unsoundness, nor how deep it is.

I mention ZFC because modern mathematics is mostly done within that framework.

But as I told MatheinBoulomenos in the above conversation, I believe most mathematical results to date (excluding set-theoretic results) can be cleanly separated into mathematical content and foundation-specific content, but this is a necessarily vague notion.

Leaky Nun

10:27

I see

user21820

I am somewhat confident that full higher-order arithmetic HOA (where each order is its own sort and you can't mix sorts) is sound in the sense that we will not find a (human-scale) proof over HOA that HOA itself is unsound.

So I would say that everything in mathematics that can be stated and proven over HOA should be safe.

Secret

Some random thoughts:

Approximation property

In mathematics, a Banach space is said to have the approximation property (AP), if every compact operator is a limit of finite-rank operators. The converse is always true. Every Hilbert space has this property. There are, however, Banach spaces which do not; Per Enflo published the first counterexample in a 1973 article. However, a lot of work in this area was done by Grothendieck (1955). Later many other counterexamples were found. The space of bounded operators on ℓ 2 {\displaystyle \ell ^{2}} does...

Unless I overlooked something in countable space, one of the things that will happen in uncountable spaces is that there exists objects that are not the limit of a sequence of finite versions of said object

I wonder how we handle these objects in a predicative setting..., cause e.g. bounded linear maps are really ubiquitous in banach spaces

> In conclusion, a formal system could have a rather small description, but have an inconsistency whose proof is so long that we can never ever store it in the physical world...

also lol at reading that statement

It kinda reminds me of those "tricks" where a person will say "yes it is possible, but it happens in a way that it is basically impossible" they are often my favorite because of how difficult is to circumvent them in negotiations

user21820

10:49

@Secret Well note that the countable/uncountable distinction is separate from the predicative/impredicative distinction.

We can still prove rather 'general' facts, such as every well-orderable field has an essentially unique algebraic closure. What may be a problem is that we may not be able to construct many well-orderable uncountable fields.

And some uncountable fields we may not be able to well-order.

Secret

One thing that lead me to that thinking direction is how uncountable sets can be proved to contain uncomputable numbers, thus uncountable objects are usually uncomputable. We also discussed some time ago in the past that it is often good enough to say that impredicative is pretty much the same as uncomputable, even in practice there is a slight distinction

Ah I see, so the constructive aspect can break down in general

user21820

So the countable/uncountable distinction does not immediately imply a problem, except that by "S is countable" it literally means we have a function from N onto S or an injection from S into N. In ZFC these are equivalent, but even in a foundational system where these differ, both still are direct ties from N to S, so uncountable collections are of course going to be much less friendly.

Secret

If S is uncountable, then it means N is not onto S. Predicativity will require us to not diagonalise the whole universe and only (forgot) using the naturals, so that means one thing that will arise is that objects in S-N will often become not constructible because we cannot in general compute the membership of the objects in S

user21820

@Secret That's not the reason, because I can't understand what you are saying. Haha half-joking...

The real reason is that when you have a tie from N to S, you have some control over S, such as you can enumerate S or you can label S or something like that. When you have no tie from S to anything else, you simply have no control over S, except in certain systems like ZFC where you somehow can tie it to some ordinal.

Secret

11:05

and for an object in an incomplete uncountable space which no sequence of finite objects can converge to it, then that will be an example of something that has no ties with N?

user21820

@Secret Possibly.

Secret

(Well, I cannot came up with a space where no elements have a sequence of finite objects converge to it, cause most of the banach spaces being used are often nice enough meaning most of its elements can be converged to by some finite sequence, so coming up such an example will be a bit ad hoc and not align with our aim for checking whether a foundation gives useful maths)

user21820

@Secret Exactly.

Secret

A few weeks ago, I read a blog post written by a chinese student which talks about the relation between foundations and mathematics. He mentioned how we don't start with axioms. Instead, mathematicians first start with some mathematical object of inquiry or some phenomenon in the real world that they want to describe, they then translate all of that into logic and from that out comes the axioms that allow said objects to be described

so axioms and foundations, in a sense, is a framework we use to give descriptions (semantics?) to the mathematical objects

Before I read that post, I kinda have the whole thinking upside down, as in, trying to find axioms, and then it somehow generates the maths we want

user21820

11:28

@Secret Correct. That was how mathematics was initially developed. It is a bit different in modern mathematics, because some mathematicians treat it as a formalistic game just like finding out whether some chess position is a winning or losing position.

That's also why I have no choice but to exclude set-theoretic results from my claims above, because they are of course extremely sensitive to the choice of foundations.

Secret

I like that more general approach. We are being locked into the thinking of set theory so much thus it is always nice to be able to step out of it and see the fuller picture

Oh, and the way you said that, it kinda reminds me there is a similar relation between modern art vs traditional art. Traditional art focus on the aesthetic of physical entities such as an object, a person or a scene, and capture that moment along with the emotions into a canvas or a sculpture. Modern art, meanwhile, are interested in expressing an idea mostly, which is why they can look so arbitrary to an unaided eye, because concepts can have a variety of physical representations

Now... I am starting to wonder, if modern maths as a formalistic game is already quite far away from reality, what will postmodern maths look like

link.springer.com/chapter/10.1007/978-3-319-12688-3_68

Actually, that reminds of a MSE: Our usual/popuar approach to modern maths is pretty much postmodern anyway

user21820

@Secret I would warn you that anything to do with deconstructionism is rubbish, and postmodernism is often quite close to that.

Concerning art, an example is that there was one painting that was simply the result of splashing a bucket of paint on the canvas, that sold for a huge sum. Clearly, both the critics who thought it was an excellent artistic expression, and the buyer who wasted the huge amount of money, had gone nuts.

Secret

[Jackson Pollock](https://www.apartmenttherapy.com/jackson-pollock-painter-physic-150631) ?
Well, while I do appreciate fine art, I never buy them, because the only thing that is really usable to me, is the idea embedded in the artwork itself (and perhaps a few strokes and techniques) thus buying the physical object for me is meaningless

user21820

Much of mathematics today still remains rooted in concrete questions. Only modern set theory is really a matter of the symbol-pushing game called ZFC.

For example, Riemann's hypothesis can be stated as an arithmetical sentence, and so most mathematicians ought to believe it has a definite truth-value. And it has many consequences on other facets of number theory.

Analysis is still very much about real numbers, if you don't concern yourself too much with general topological spaces that aren't metric spaces...

And so on.

Applications of mathematics in the real world will always invite exploration in mathematics that is tied to the real world.

Secret

11:45

> general topological spaces that aren't metric spaces

Leaky can tell you how easy I tend to explosively generalise and abstract things in my thinking, which is why the above description of each maths domain only occured to me when my thinking is using the more applied maths side (continue to the next message)

famesyasd

Hello guys! Sorry to interrupt you again
@user21820 I finally came to read the thing about definitions that you've linked to me back then (it was a little bit over my head before) https://math.stackexchange.com/questions/1863150/how-could-we-formalize-the-introduction-of-new-notation/1864310#1864310 this one

I haven't read the step about functions yet but about predicates and constants: we can add a new predicate without restrictions right? and for constants we can add multiple symbols for a same formula, say, for the empty set we could have also another symbol such as $\varnothing$ along …

Secret

Having said that, applied maths does gain a very significant boost recently with the increase in importance of the data sciences, so maths is a lot more intwined with real world applications compared to e.g. back in the 18-19th century

user21820

@famesyasd Right; predicate-symbols can be added without restriction, as long as you add just one axiom for each new predicate-symbol to 'define' it.

@Secret By the way, it is often claimed that people did not know the usefulness of number theory until cryptography, and likewise esoteric stuff in ZFC set theory may become useful in the future. That analogy is totally wrong. Number theory was about natural numbers, which have an approximate embedding in reality. ZFC, on the other hand, nobody has yet to show me even a conceptual approximate embedding into reality.

@famesyasd To say more, note that you obviously cannot add two conflicting axioms 'defining' the same new predicate-symbol. And you can only add an axiom of the form stated there; "forall x,...,y ( P(x,...,y) iff ... )", for each new predicate-symbol P.

Secret

One big issues of ZFC are the infinities, there is simply no known candidate matter-energy in reality that can represent that.

There was once a theoretical arxiv paper in 2012 in particle physics of someone trying to use ZFC stuff to justify the probability of producing a higgs boson with some mass, but I think that's way too ad hoc or something.

user21820

@Secret With 99.9% confidence it is a crank paper by cranks. Without even looking at it.

@famesyasd: And for constants yes you can add new symbols for the same object, but it's not necessary that your symbols would refer to the same thing. In the case of ZFC and the empty-set, it is true that you can prove "exists unique x ( forall y ( not y in x ) )", so if you do add constant-symbols for that object they will be provably equal. But in general you may not be able to prove or disprove that two added constants are the same.

Secret

11:54

(The following is a series of 3 messages, thus do not comment until all 3 are posted)

https://math.stackexchange.com/a/1295309/180683
> Now, all that being said, ZFC does find uses outside of mathematics. In particular, it gives us an entirely unambiguous language to work with, and for that reason provides a great foundation for talking about such objects as recursive/computable functions and Turing machines. So there are certainly applications directly to (Theoretical) Computer Science, for one.

But we can do computational theory without ZFC just fine

> If one thinks of set theory as the "study of infinity", then it has further applications, particularly in the subjects of analysis and topology. Making precise what is "infinite" allowed us to understand the idea of convergence of series. Here we also find results that depend on (usual weaker versions of)
the Axiom of Choice, and plenty of arguments, examples, and counterexamples that depend quite heavily on the idea of cardinality. Heck, the basis of several important counterexamples in topology is the first uncountable ordinal, ω1.

We don;t need that to understand convergence

and we already shoot down $\omega_1$ ages ago

user21820

That's 5 messages, not 3. Tsk tsk...

Haha..

Secret

yeah I overshoot

user21820

@Secret That answer seems to be by a poster who does not really know the alternatives to ZFC. Saying that ZFC provides a "great foundation for talking about such objects as recursive/computable functions and Turing machines" seems to be stretching it.

As for infinity, I think all that ZFC does is to allow people to understand the concept of 'infinity' defined in ZFC itself, not that ZFC can capture something that is really 'infinity', whatever that may mean.

Secret

But yeah, while I still really love infinities (with my most recent ramble in Rambles being playing with something that is between finite and countable (only to prove that it is inconsistent shortly after, disappointingly)), if we put on the thinking hats that "maths should describe reality", then I see no place for any actual infinities in our world (sadly)

@user21820 I guess the only notion of infinite we can grasp independent of foundation is potential infinity, the notion that something becomes unbounded

it is used from the natural numbers to induction and recursive algorithms

user21820

@Secret Yea so you can play with mathematical notions as you play all sorts of games. Some like ZFC produce elegant theorems, but hopefully not contradictions otherwise all the elegance is useless unless you like elegant contradictions heheh..

@Secret Yes the notion of unboundedness is very much an arithmetical notion.

famesyasd

12:03

@user21820 ye ye ye, ty I thought about all of that too, thank you for confirming it Also about fitch style and the constant' rule, we should add some restriction for upcoming formulas $\phi(c)$ because if we just use them as axioms we might accidently awake $\forall$ intoduction rule, might we not? in forallx he uses indentation for \exists elemination rule so I thought we should restrict these axioms so that they only can be used as non assumption sentences

Secret

Actual infinity, I suspect, its essence is it captures the notion of unreachable (but the knowledge I have for reference is really just ZF, ZFC and IST (all are set theories)). But if that is true, then its very definition makes it an incomplete notion, because by defintion, no system can prove its existence from the inside / or from below

user21820

@famesyasd For constants, it is okay because the new constant-symbol is not a variable.

famesyasd

but we do use \forall introduction rule for constants exactly, don't we?

user21820

No that's not allowed. If it is unclear in forallx, you can refer to my variant:

5

A: Predicate logic: How do you self-check the logical structure of your own arguments?

Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preser...

It's nearly the same as the one in forallx, except that my exists-elim rule is slightly different. I permit creating a fresh variable for the witness like in a programming language.

It makes it slightly more complicated but the advantage is that it is more natural.

In other systems like the one in forallx, the forall-intro rule can only be applied to free variables, because you want to essentially claim that it holds for any object (represented by the free variable).

In my variant, there are no free variables at all.

@famesyasd: If anything is unclear please feel free to ask. It is best if you get the intuition behind these deductive systems, because the details are never so easy to remember or get right, but if you understand the reason then you won't get it wrong in practice.

famesyasd

@user21820 yeah, I was typing xd wait, I'm confused now that's true. I might have misunderstood some rules for quantifiers in fitch haven't really worked through them
but I thought if we have proven Gd->Gd for example, and we can do that without any assumptions so we can now use universal introduction rule to gain \forall x Gx->Gx for example but I fail to see what Gd->Gd has to do with variables at all, it has no variables whatsoever, it has one name howver (is it the same thing as constant?)

user21820

12:15

No a constant-symbol is not a variable, and you can only do forall-intro on free variables in forallx's kind of system. His book has section 19.1 stating the kinds of syntax.

@famesyasd: Okay I see the problem. Unfortunately, that forallx book is not as good as I thought.

famesyasd

what?! xd

user21820

So it's not your fault.

On page 147 it says "The crucial thought here is that ‘a’ was just some arbitrary name." despite saying in 19.1 that "a" is a constant. It did not make clear that this arbitrary name must not be a constant-symbol.

So it is natural for any reader to think that it applies to constants, as you did. That is, however, wrong.

famesyasd

lol

user21820

For example, take a look at this axiomatization of PA.

It involves the language of arithmetic, which often means including 0,1,+,·,<.

0,1 are constant-symbols, and +,· are binary function-symbols, and < is a binary predicate-symbol.

PA can prove "0 < 1". But certainly PA should not prove "forall x ( x < 1 )".

famesyasd

mmm

user21820

12:22

Do you get the point?

famesyasd

ywah i need to reconsider and check that myself

but yeah I saw where you were going when you typed 0 and 1

user21820

Haha great!

famesyasd

xd

is it actually true that zfc without axiom of infinity is consistent?

user21820

@famesyasd Well it is consistent relative to PA, meaning that if PA is consistent then ZFC minus Infinity is consistent. We can't possibly ever prove non-circularly that PA is consistent, so I don't know if this answer is satisfying or not.

famesyasd

12:41

@user21820 that's offtopic but you are not a native english speaker! right? :)

user21820

@famesyasd I am a native English speaker. There are many different dialects. What did I say that made you think I wasn't one?

famesyasd

damn! really? well then you are a first native enlgish speaker that uses "= )" emote then

user21820

Lol...

famesyasd

I really haven't ever met anyone who uses that emote and is also not from some Russia-like country

user21820

13:25

@famesyasd Sorry had to attend to something just now. Heh emoticons are not a good way to guess geographic location. =)

@Nathaniel: Hello and welcome!

famesyasd

15:27

@user21820 you here?

user21820

Yup, for a while more.

famesyasd

okay, so I started reading your rules, but first I need to understand the difference between variable and names, also, what is a constant? (constant = name I guess) I think I understand all the rules from TFL in fitch style so I need to understand those for quantifiers first (aside from that x \in S and types in your rules)
To ask first: Does universal elimination give us a name or a varialbe? or is it a name but also a variable? so something like variable-name or something lol I mean it seems we manipulate it as an object but also implicitly assuming it is general as variable, I guess it's…

user21820

@famesyasd In my system, I only specified about variables, so that it is applicable to different kinds of logics. For first-order logic, we still have constant-symbols, predicate-symbols and function-symbols, all of which are separate from variables. These terms are standard, so I won't use strange terms like "name".

A constant-symbol refers to an object. A function-symbol can be applied to any object to yield another object. A predicate-symbol can be applied to an object to yield a truth-value.

famesyasd

a, okay, it's just that it was used in that book, names also refer to objects, one name can refer to maximum of one object at the time, but objects can have multiple names

user21820

Since that book used "name" for variable, it does not seem good to try to phrase things in terms of that book's terms.

We must distinguish between constant-symbols and variables. The former are part of the first-order language, and so in any context will already refer to some fixed object.

The latter are used for quantification like in "forall x ( ... )". In my system every variable must be declared before it can be used. Are you familiar with programming?

famesyasd

15:42

ehm

I mean If I say yes, then what level of familiarity are you referring to? :D

I don't know about types, are they from programming?

lol

well I can say yes, I'm familiar with programming at the very very basic nooby level

I know about variables I guess if you refer to them as those from programms

user21820

@famesyasd Well types are not really the same as those from programming. Yes I was referring to variables as like those in programming languages where you must declare before using.

famesyasd

yeah, okay you can explain it with programming then

I'm completely lost about types tho

yeah, okay you can explain it with programming then

damn my internet is dying

user21820

There are two ways you can declare them. Either by a universal subcontext, represented by the rule ∀sub, or used in the ∃elim rule to refer to the witness that the existential statement is true (also called existential instantiation).

famesyasd

do types mean something like: x is natural, or y is integer or theta is matrix that kind of thing?

user21820

@famesyasd Yes.

The universal subcontext corresponds loosely to "for each x in ..." in programming and the existential instantiation corresponds loosely to variable assignment in programming.

These are the only two ways I allow you to declare a variable. And like in some programming languages, I forbid re-declaring a variable if it has already been declared in that context.

This prevents confusion.

That is what I mean by "unused variable x".

famesyasd

15:52

okay, wait, let's start from the beginning: so I can introduce a new variable alone in my proof? with the use of your two rules or something

user21820

Let us go through the example in my post.

If ∃x∈S ( ∀y∈T ( P(x,y) ) ):          [→sub]
  Let a∈S such that ∀y∈T ( P(a,y) ).  [∃elim]
  Given z∈T:                          [∀sub]
    P(a,z).                           [∀elim]
    ∃x∈S ( P(x,z) ).                  [∃intro]
  ∀z∈T ( ∃x∈S ( P(x,z) ) ).           [∀intro]
  ∀y∈T ( ∃x∈S ( P(x,y) ) ).           [∀rename]
∃x∈S ( ∀y∈T ( P(x,y) ) ) → ∀y∈T ( ∃x∈S ( P(x,y) ) ).  [→elim]

The indentation is exactly what you expect it to mean from programming.

famesyasd

Can I think about indentation as like using begin..end or something?

so it starts a new blocks and it finishes this block when we step back

user21820

Yes exactly, and also for if-structures.

The first line is an if-subcontext, and like you would expect, all the indented lines underneath it are only valid in the context where that if-condition is true, namely "∃x∈S ( ∀y∈T ( P(x,y) ) )".

Only the last line is at the outermost context, which is understood as meaning "in every context".

In this system every statement that can be written in the outermost context is true in every context, and these statements are called theorems of this system.

So in the above proof there is only one theorem, namely the last line, "∃x∈S ( ∀y∈T ( P(x,y) ) ) → ∀y∈T ( ∃x∈S ( P(x,y) ) ).".

famesyasd

is there a typo in your next-to-last sentence? I'm having trouble translating it

aa, okey

user21820

Got it? I was about to rewrite it with brackets haha..

famesyasd

16:00

okay, wait a minute

let's say I have the following proof:
A
...
A
so to understand for myself I shall rewrite it as follows
begin
A
...
A
end
correct?

user21820

What programming language are you familiar with? It's easier to use an actual language.

famesyasd

and for implication I have
If A
....
B
A->B
what does that mean in terms of my begin-end?

pascal, c++

user21820

Ok I know C++ so we'll use that.

Let's get propositional logic done first.

famesyasd

okay

user21820

→sub corresponds directly to an if-structure. That rule merely says that at any point in the program we can insert an if-structure with any condition that is well-defined at that point.

And additionally, that rule says we can assert the chosen condition inside that if-structure.

famesyasd

16:04

example!

user21820

This correspond to:

if( A )
{
  assert A;
}

You know assert, right?

famesyasd

ehmm

I don't think there is such a keyword in c++..

user21820

It's standard C language.

famesyasd

ehmm

user21820

If you run the program, then when it asserts something it will continue if the asserted expression evaluates to true.

But if the asserted expression evaluates to false then it will throw an assertion error.

Got it?

famesyasd

16:06

aa okey

got it

okay*

user21820

The goal of a logic system is to ensure that we never assert any false statement in its context.

This corresponds to writing a program that never makes an assertion error.

Check that the above program corresponding to →sub never makes an assertion error no matter what A is, as long as A is a well-defined boolean expression.

famesyasd

example!

user21820

3 mins ago, by user21820

if( A )
{
  assert A;
}

famesyasd

what is a boolen expression? formula from tfl?

user21820

It means in the programming language.

famesyasd

16:08

what is A? a variable or formula? (formula concerning variable named a?

user21820

A must be a boolean expression in the programming language. I don't want to be too precise here, because otherwise you also need to have a "main" function and all that. Just pretend this is like an abstract kind of C++.

The point is that the program will test whether A is true, and if it is true then it will execute what is inside the if-A-structure.

famesyasd

wait, for that part, so I can write something like
if (x > 0)
{
assert (x>0)
} ?

user21820

Yes you can write that inside a context where x has been declared.

The idea is simply that if A is true then the "assert A" is valid, and if A is false then the if-A-body is never executed in the first place.

famesyasd

but the truth of A depends on x

or we use only sentences wuthout free variables?

user21820

Yes, that's why I said every variable must be declared. For example:

for(int x=0;x<10;x++)
{
  if( x>3 )
  {
    assert x>3;
  }
}

famesyasd

16:15

declared means having some evalutation i.e. we for sure have x=3 or something

?

or simply stating that we have empty for now variable x for which no values have yet been given

user21820

In C++ you cannot use a variable that has not been declared; that will give a compile error.

So I don't understand your question.

famesyasd

aa, okay so we run the programm also

user21820

The point is that without running the program you can see why the program above (with the for-loop) will not make an assertion error.

Right?

famesyasd

my internet died sorry

yeah, if it's correct then it passes the assertion check, if it's false then the if cycle will never be passed

user21820

That is exactly the kind of reasoning we will use in this logic system.

You could say it corresponds to the following proof:

forall x in [0..10]:
  if x>3:
    x>3.

Is the idea behind this system clear now?

famesyasd

16:25

I'm rereading now

user21820

I still haven't got to the details, but the fundamental idea is that we want every sentence we write down to be true in its context.

To do so, it suffices to ensure that each rule is sound, meaning that, if what we have already written satisfies that every sentence is true in its context, then what the rule allows us to write next also satisfies that every sentence is true in its context.

We have just discussed the reason that the →sub rule is sound.

You can slowly check one by one that the other rules for propositional logic are sound.

In case it's not familiar to you, "⊥" stands for a constant false statement, which in programming would be just "false".

One rule worth explaining is the ¬intro rule.

famesyasd

once again, what does "true in its context" mean? more precisely the word "context"?

user21820

The "context" here refers to all the context-headers that govern that statement. You get this by tracing the indentation.

I wrote in my post: "The context of each statement is specified by all the headers that are in effect.".

famesyasd

mm, okay, got it

user21820

Ah good. It's a bit troublesome to explain, so if you get it then I don't have to go into detail. =)

famesyasd

16:36

and what's wrong with \not intro rule? it's simple proof by contradiction, isn't it?

user21820

It is. If you understand the program execution viewpoint, then you can see immediately why it's sound.

Because "A implies false" is essentially a 1-line form of "if(A){assert false;}", and if that is valid (in the current context), it means A cannot be true (in the current context).

A lot of people trip over this rule if they don't know the program viewpoint, because of the following valid proof:

If A:
  If not A:
    A.
    not A.
    False.
  not not A.

Does it make sense to you? It should when you 'run' the proof, and that is exactly what proof by contradiction means, no more and no less.

Also consider:

If False:
  If 1+1=2:
    False.
  1+1≠2.

famesyasd

yes, the last one does make sense as also the previous one, though I haven't checked them through your standpoint (I'll do that later) I translated them into my own

xd

user21820

That's fine. Some people have more trouble with them than others.

But the program viewpoint in my teaching experience so far makes it undeniably valid.

(Biggest problem is in teaching people who don't know any programming.)

famesyasd

okay, okay, you sold me on that for sure, don't worry :) I'll definitely check your idea later

user21820

Anyway I got to go soon. Before that, I'll tell you a bit about the types and after that I don't foresee you having any trouble to understand the rest of my post up to the "Example" section, excluding the "Notes" and "Set theory" sections.

famesyasd

16:44

does "up to" mean including the example section or excluding them?

user21820

Including the example section.

famesyasd

okay

user21820

Basically, for now, you can just assume that you only have one type, which in my post is called obj. The universe rule essentially says that every thing is an "obj". Because of that, there is effectively no difference in saying "forall x in obj ( P(x) )" and the usual "forall x ( P(x) )" in standard first-order logic. The reason I choose to have this notation (called restricted quantification) is so that it is much more in line with our intuitive thinking.

For example, it is intuitively clear that "not forall x in S ( P(x) )" is exactly equivalent to "exists x in S ( not P(x) )".

For an informal example, "not every person is a dictator" is exactly equivalent to "some person is not a dictator".

famesyasd

wait, which notation is moore in line with our intuitive thinking, the one where we are implicitly assuming abject type when reasoning right? instead of FOL one

user21820

Restricted quantification is more in line with our intuitive thinking.

famesyasd

16:51

restricted quantification is when we are assuming our object type?

user21820

Sorry I guess I was not precise with what I said.

famesyasd

like let x be an interger or (for all x (where x are integers or sets or objects or something) this one? instead of just \forall x it is Px as it is in FOL

user21820

The "in S" part of "forall x in S ( P(x) )" is why we call it "restricted quantification".

famesyasd

mhm

okay

agree

user21820

In ZFC over first-order logic, the conventional way is to interpret "forall x in S ( P(x) )" as a short-hand for "forall x ( x in S implies P(x) )".

famesyasd

16:52

right

user21820

This is unwieldy because "exists x in S ( not P(x) )" would be short-hand for "exists x ( x in S and not P(x) )". The nice symmetry is broken.

Anyway that's really all there is to restricted quantification. It is a syntax thing, and so does not depend on any set theory. That's why I called "obj" a type, not a set.

If "obj" is the only type you have, then you can effectively not write it because it's not actually restricting anything.

famesyasd

mhm

user21820

What is interesting is if you have other types like Nat or can form more types from existing types.

famesyasd

Nat?

user21820

Natural numbers.

Just for example, remember I mentioned this axiomatization of PA? It is completely compatible with my system, where N is a type.

famesyasd

16:56

so it;s like given to you at the beginning or do you create it from Obj or something>

user21820

In this case, we would need to include it at the beginning.

famesyasd

instead of Obj? or along with Obj?

and we also can create more types from the existing ones? like type Even from Nat

user21820

Along with obj. In conventional first-order logic, PA is described as having its intended domain be only the natural numbers. But if we don't want to force such a viewpoint, we can have both types, obj and N, and use those linked axioms to describe N.

famesyasd

okay

also, that might be slightly offtopic, but I've heard something about category theor, do you also have types there or no? or were they called categories

and also when it's useful to start learning a bit of category theory if I'm first year undergrad right now

user21820

Category theory is a framework that can be used to study certain algebraic objects and structures. I think it's not necessary for you to learn about it at this point, since it's not exactly as 'super' as some people make it sound.

It's just a framework, and good for describing some things, but not really necessary especially at the undergraduate level.

famesyasd

17:03

I forgot what framework was

user21820

I'm using it with the English meaning.

famesyasd

I don't understand it's meaning as an english word too:(

user21820

Okay here's a mathematical example.

You know the group axioms?

famesyasd

yeah

is it a framework?

so any composition of axioms (including FOL) is a framework?

user21820

They describe every group. This means that if you want to study some kinds of groups you could prove some theorems within the theory of groups, and 'come out to the meta-system' and know that those theorems apply to all groups.

famesyasd

17:06

yeah, btw do we only know this only as a metafact? that these results apply to all groups

user21820

Yes, because the theory of groups cannot talk about any collections.

In modern mathematics the meta-system is ZFC set theory, which can talk about structures like groups.

But typically textbooks and teachers don't mention the meta-system, so you 'learn' to work within an informal system.

That is not always good in general mathematics, and it is always bad in logic.

famesyasd

where can I read about this? in Rautenberg?

user21820

I just checked. Rautenberg does not explain this either. Hmm.. I'll explain to you next time.

@famesyasd: Got to go now! See you!

famesyasd

okay!

thank you!

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic