Logic - 2017-12-16 (page 2 of 4)

Leaky Nun

06:00

I thought natural number equality is decidable

user21820

It is, but quantifiers are not.

Leaky Nun

eg?

David Reed

you can alternatively replace "basic computability" with "everything of interest in continuous mathematics"

user21820

You need one unbounded quantifier to define the halting problem.

David Reed

@secret You certainly have a way with words

user21820

06:01

@DavidReed You should go look at his secret room.

David Reed

hahaha

the "rambles" ?

Secret

I have 3 SE chat rooms, btw

user21820

I frequently call out on some of his rambles that really can't make sense. =)

Secret

NB: I made up that word: Metropolis Algebra. It is basically an algebraic structure that includes all possible algebraic structures (NB no I have not thought seriously about whether I want it to include itself and its negation (whatever that means))

David Reed

whats "NB" stand for?

I see you use that alot

Secret

06:04

9

Q: What does N.B. stand for?

I have received letters for years, and some of the most common things in letters are post-scripts, however, there are also these funny little "N.B." which obviously do not stand for Post Script. What are these letters and how are they used?

I basically use that as a short form of Note or Footnote

David Reed

gotcha

Leaky Nun

nota bene, "note well"

Secret

I am kinda like the borg in some way, in that everywhere I visit it will become a time capsule for me to check in the future

Put it simply, my whole internet footprint mostly consists of notebooks everywhere I go

David Reed

Yes the term "metropolis algebra" was part of what I meant. You have a flare for dramatic, expressive, poetic language

Secret

Well, I use "metropolis" as a descriptor because if that algebra can really be built, it will be literally a city where you can easy move from one algebraic structure to another, as if they are just buildings

David Reed

06:07

You are in search of category theory my friend

Secret

Almost everyone said that, lol, someone in the math chat even said one of my rambles is a sign of rediscovering concrete category theory

David Reed

either that or universal algebra yes

Leaky Nun

@user21820 do you basic category theory?

we should have a category of propositions with the morphisms from X to Y be proofs of X -> Y inside the system

Secret

My 3 chat rooms are: Rambles, Mathworks and SecretLabs SE Branch. Please do note some kind of Eldritch Abomination live in the 3rd one, lol

user21820

I've looked at it before and it does not seem to offer anything that cannot already be done in ZFC, and I'm not a fan of ZFC. Note that it's just a matter of perspective, not strength. The only argument for category theory over ZFC is the nativeness of morphisms, but that doesn't seem very well motivated to me.

It's good for when you do want to talk about morphisms of the typical algebraic sort.

Or similar structures.

But since that can be done internal to ZFC, why bother using a separate system?

David Reed

06:14

@Secret A good place to start for you I think would be Gallian's "Contemporary Abstract Algebra"

Secret

Categorical logic

Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor. The categorical framework provides a rich conceptual background for logical and type-theoretic constructions. The subject has been recognisable in these terms since around 1970. == Overview == There are three important themes in the categorical approach to logic...

user21820

@AliciaIsabelQuaini: Oh hello didn't notice you dropped in here. Feel free to join the discussion or post any inquiry about (mathematical) logic here.

@LeakyNun: To clarify what I said, within ZFC you can easily consider a first-order theory CT capturing category theory, and then when you have a structure that you can show is a model of CT, you can then apply any theorem of CT onto it. So you can do most of your work inside CT, and then pull the results out to models of CT within ZFC.

David Reed

I should mention, ironic as it is, most mathematicians are utterly and completely disinterested in formal mathematical logic. Their interest in CT is independent of anything having to do with foundations

However

since it has been brought up

here is something I think would be difficult inside of FOL

Commutative diagram

In mathematics, and especially in category theory, a commutative diagram is a diagram such that all directed paths in the diagram with the same start and endpoints lead to the same result. == Importance == Commutative diagrams play the role in category theory that equations play in algebra (see Barr–Wells, Section 1.7). == Description == Parts of the diagram: objects (also known as vertices) morphisms (also known as arrows or edges) path or composition === Arrow symbols === In algebra texts, the type of morphism can be denoted with different arrow usages: monomorphisms with a ...

go to proof by diagram chasing

user21820

I don't understand what you mean by "difficult". Of course anything that involves humans musing over diagrams is 'hard' to represent in any formal system, not to say first-order logic.

David Reed

Yes but theorems of interest are proved that way

user21820

06:26

Don't even need to go so far. Just take any proof from graph theory.

Or, millenia ago, Euclidean geometry.

David Reed

I actually think you could do Euclidean geometry in FOL

user21820

Even Hilbert, thinking he had succeeded in formalizing that geometry, had actually failed.

It was discovered much later that a lot of his deductions were based on intuition and his proposed axiomatic system was actually insufficient!

David Reed

Well admittedly I've never tried, just going off the flavor of proof I did in undergrad geometry

In any event, we were talking about CT, which is why that was the direction I went in

user21820

@DavidReed Just to give an example of that sort, you would have shown that the angle at centre of a circle is twice that subtended at the circumference.

But your proof or your teacher's is almost certainly incomplete.

David Reed

I'll find the text at some point and give it a closer look

user21820

06:29

And when you try to make it rigorous, you find that you need notions like "on this side" and "on that side" and you will realize that the whole business is not actually formal.

I have a way out of it, and it is decidedly not in Euclid's style. I use directed angles instead.

So that they add up algebraically.

In fact, diagram chasing in category theory should be much easier to formalize than Euclidean geometry, because it can be easily formalized algebraically (even though the result would be hardly as pleasant to read as a diagram).

David Reed

I personally think it would be irresponsible for a mathematician to disregard the notion of a visual proof as universally unacceptable

user21820

@DavidReed Please rephrase. Too many negatives are ambiguous.

David Reed

some visual proofs are acceptable

depending on context

I do not agree with the statement " A visual proof is never acceptable as a method of proving something"

user21820

Visual proofs are not acceptable as rigorous proofs. But they are typically useful, nearly necessary, for finding rigorous proofs.

David Reed

then you and i disagree :)

user21820

06:34

There is no such thing as a rigorous visual proof, unless you specify a fixed format for the diagram.

And the format itself is part of a formal system.

David Reed

Then you would be very displeased with category theory :)

user21820

No, you do not understand how formalism in mathematics works.

See this post:

2

A: When is a proof or definition formal?

There is actually a whole spectrum of "formality" in mathematics. In informal terms, "formal" it refers to what is considered as rigorous, but that is of course subjective. Absolutely formal: Written in a language that can be verified by a program that implements some formal system. Check out M...

David Reed

it is a matter of what I personally accept as a proof of something

I wouldn't accept a geometric proof in real analysis for instance

I have no issue with diagram chasing

user21820

Well if you have read my post, I classify diagrams (generally) as "somewhat informal". Certain diagrams that follow standard conventions (which seem to be the case in category theory) can be considered "reasonably formal":

> Reasonably formal: Written in the standard of modern mathematics, that is, in sufficient detail to convince experts in that field of mathematics that it is rigorous and correct. Lots of steps may be skipped, and yet it may be considered perfect.

David Reed

there are contexts where I consider a visual proof as having "sufficient detail" to convince me

user21820

06:40

Exactly.

Isn't that what I said, in my self-quote?

David Reed

I'm quoting your quote

user21820

So it falls under my classification of "reasonably formal", but note that it is a few steps down from what I consider as absolute rigour.

Nearly all mathematics papers are written at a level of formality somewhere between "reasonably formal" and "somewhat informal".

That is why some people doubted Hales' proof of Kepler's conjecture.

David Reed

That's correct, nobody does proofs within a logical system as its simply impractical

That reasoning is conditioned into them, so when the small class of mathematicians that are really anal about it and go back and check it that way, errors are rarely found

Leaky Nun

> really anal about it

David Reed

I have read however that recent advancement in topology and (surprise) cat theory have been found to not be first order expressable

hence the interest in finding a new foundation

I don't mean anal in a bad way

I mean tedious really

user21820

06:45

@DavidReed Errors are rarely found?!

Errors are often found!

David Reed

I'm not aware of any major results that have been disputed

I could be wrong

Please link me

When I say errors found btw, I mean found by expressing everything in a first-order system and using rules of inference formally

I don't mean: hey this leap you're making here is unjustified

user21820

Typically it's not so bad that the result is disputed, but that significant gaps are found. Like my example of Hilbert's axioms for Euclidean geometry. Even when Hilbert was attempting to be very formal, he failed and it took someone later who was even more strictly formal who found missing axioms needed.

David Reed

That fair, really I mean what appears in modern journals

user21820

In modern journals, there was a wrong proof of the 4-colour theorem that remained unchallenged for a decade I think.

Then later the computer-verified one was challenged, but actually was correct. So ironic.

There are many examples, but I don't store them in my head.

David Reed

I think it would still be consider rare in relative terms relative to the number of results published each month/year

user21820

06:51

Heh someone already asked this on Math SE.

10

Q: List of proofs of non-trivial theorems which were unnoticed to be wrong for at least a few years

For example, the Weber's proof of Kronecker–Weber theorem. I would like to know such proofs. It seems to be important for me to remember that a widely accepted proof might be wrong.

reference-request soft-question math-history examples-counterexamples big-list

@DavidReed I think significant gaps often occur, but wrong results are rare because intuition has some tendency of getting things right even with the wrong reasoning...

The top-voted answer in the first linked MO thread is real funny:

> [...] Zhang may be perhaps the only person to have published in such a prestigious journal both that P and that ¬P!

David Reed

In the past 10 yrs, more math has been published than a single person could learn in a lifetime.

Let's make it 25 to be safe

Leaky Nun

> Let's make it 25 to be safe

RIP "10 yrs" 2017-2017

David Reed

So the term relative here has serious implications. In any event, what I had really meant is that the avg mathematician will consider a proof in paragraph form as having "sufficient detail" to convince them.

I wouldn't be surprised if I could make it 5 yrs leaky and that still be true

user21820

@DavidReed Of course. Nobody here doubts that the vast majority of modern mathematician will be convinced by some paragraph proofs, and won't even want to read a more formal proof.

The thing is that that always carries a small but significant risk of significant error, though the result is usually salvageable.

Though the MO post names examples that were not salvageable.

Here's another funny quote from that comedic thread:

David Reed

I will stipulate that the small subclass of "anal mathematicians" serve a crucial and indispensable role

user21820

06:57

> Dirichlet's better definition of function, blew the whole work of Lagrange apart, although in a reverse historical sense Lagrange was saved since the title of his book is "Theory of Analytic Functions..."

David Reed

I'm just disinterested in being one of them :_

:)*

user21820

Yea.

Today they are mostly working in Coq, Mizar or HOL Light.

But even Coq adherents mostly admit that Coq is write-only (it is not human readable).

Mizar is human readable, and based on ZFC plus Grothendieck universes, so if you are ever interested you can take a look.

HOL Light was recently used to prove Kepler's conjecture, so everyone is now satisfied.

David Reed

@user21820 I find it quite depressing that you are a comp scientist and I am a mathematician and you know more about MATHEMATICAL logic than I do :)

user21820

@DavidReed I did two degrees.

David Reed

two master's?

user21820

07:00

Undergraduate.

But my logic knowledge doesn't come from school.

And Leaky knows 10 times more than I did at his age.

David Reed

Mine either really, I did intro and intermediate logic (and also most of legal logic before dropping) but that was it

user21820

There's always a younger fish. =P

David Reed

I was at the pinnacle of my knowledge of academia at 23

Every year I lose a bachelors degree worth of information to memory loss

Secret

Progress on the exercise: The If A is easy, it is the If not A that is harder. Still experimenting

user21820

@Secret Good to experiment!

David Reed

07:06

Interesting example: I will accept a truth-table as a visual proof of small sentential statements

user21820

@DavidReed Aha but you recognize that it is circular, right? Namely you have to be able to use your eyeball to look straight along each row/column, and somehow convince yourself that you have listed all the possible truth assignments.

Secret

this is a lot better than my current PhD data analysis progress. It seems that pandas software have no in built way to pair up elements with their indices flipped

and I am trying to figure out a way to minimise for loops

David Reed

@user21820 That's what I mean. I consider it to have "sufficient detail" to convince me

user21820

Yup.

David Reed

the word "small" here is also relevant

user21820

07:08

We also use them to teach basic logic to students...

There is no escaping the circularity, whether by tables or by words, that if someone does not know what "if" means then there is no way we can explain it to them.

David Reed

I'm giving you an example of what I would consider to be a rigorous proof that is visual

I will accept truth-table definitions of logical operators as well

user21820

And I'm saying you can't do better than that. Every definition that anyone can give of the boolean operations, in the past and in the future, will be circular ultimately.

David Reed

In other words, some of these fitch-style deductions of really trivial statements that are being done I would accept a truth-table as being equally convincing

user21820

So might as well use tables.

David Reed

Now I follow you

user21820

07:12

And note that the point of the Fitch-style system was not to convince people of the truth of small tautologies, but to convince people of the possibility of convincing them of the truth of arbitrary tautologies. =)

When we reduce everything to a finite set of rules, and the opponent accepts them, then we can use them to our heart's content.

David Reed

I understand. This is something that just occurred to me in light of our above discussion regarding the acceptability of a visual proof

have you ever studied neuro-linguistic programming?

I find your choice of the word "opponent" interesting

user21820

I have heard of it, but know nothing about it.

David Reed

as opposed to say, "audience"

user21820

@DavidReed Oh that is just because there is game semantics that I use to explain quantifiers to students.

David Reed

Ah

user21820

07:16

"Proofs as games" under my profile:

11

A: Is formal truth in mathematical logic a generalization of everyday, intuitive truth?

Your main issue here seems to be that you are wondering how all the following statements: If the Earth is flat, then the Earth exists. If the Earth is flat, then the Earth does not exist. If there is life on Europa, then the Earth exists. could possibly be meaningfully assigned th...

David Reed

winning strategies and the like. I'm pseudo-familiar

user21820

Viewing it that way LEM is non-constructive in being like an oracle.

David Reed

I've been listening to the same live youtube video of a song since entering this chatroom lol

just realized that, kind of a random comment

user21820

Lol!

What sort of music do you like?

David Reed

do you play any instruments?

user21820

07:19

Haha yes I do.

David Reed

I'm currently listening to 25 or 6 to 4 by Chicago

oh yah? what do you play?

user21820

Piano.

David Reed

https://www.youtube.com/watch?v=7uAUoz7jimg

I played guitar religiously, it is how I permanently injured my hands. Terry Kath is one of my favorites, which I think is why I have been able to stomach this for so long

I have a strong dislike of country, death metal, and rap. I'm game for virtually anything else

user21820

@DavidReed Oh I see. Some people wear something, and use picks, right?

David Reed

lol

I feel like there was a time when pianist and guitarists worked together to make something called music

that sounded better than either instrument on its own

Secret

07:26

ok, this is not helping, I came up with the exact same proof as yours. Btw without the notion of numbers, how can we define structural induction for the 4 cases A, not A, B , not B?

David Reed

Regarding formalism of diagram chasing, It is interesting as I never really explicitly thought of it this way, but is true :

Given a commutative diagram, a proof by diagram chasing involves the formal use of the properties of the diagram, such as injective or surjective maps, or exact sequences. A syllogism is constructed, for which the graphical display of the diagram is just a visual aid. It follows that one ends up "chasing" elements around the diagram, until the desired element or result is constructed or verified.

user21820

@Secret It's great that you came up with the same proof as mine. Was it the case splitting proof, or the shorter one I posted later?

Secret

case splitting

user21820

Okay.

Good. I guess you understand better how it works.

Secret

I currently cannot think of ways to escape not A without having two levels of subcontext to generate the required A and Bs

user21820

07:31

Oh yes you forgot to remind me to tell you why there is essentially no other proof of LEM.

Secret

The rules themselves, IMO, seems to have some kind of "geometric meaning". There are rules that stay within the same context, there are rules that generate contexts one level lower and there are rules that allow escaping to a higher level context

user21820

@DavidReed Would you like links to some youtube videos of what I think is quite nice music? I don't go searching for them, so I can only give a few that I recently came across though..

David Reed

Me neither actually, was watching a Chicago documentary that had a small clip of this video, which i quite enjoyed, so went looking for it

Of course

user21820

@Secret Well yes. Though there's not really much to say about that. It's just like that.

Flower Dance ~ DJ Okawari Cover

►

(and some of her other videos)

Yiruma - River flows in you

►

(and some of his other songs)

Most of the piano pieces I like are by little-known composers, though.

Like Fifth Nocturne by Leybach.

@DavidReed: Ever heard of this one?

David Reed

leybach? negative

user21820

07:40

It's one of my favourite pieces, first learnt from a book called "Piano Pieces for Children".

David Reed

haha

Secret

A "geometric" way of thinking about the rules:
1. fixed point
2. Jump one level lower to known destination
3. At lower level, use concept from a higher level
4. Escape from a lower level to a higher level by wrapping up the lower levels
5. Use a concept from a lower level at the current level
6. Combine two concepts
7. Split two concepts
8. Generate a new concept on the left or on the right
9. Combine given two concepts into the same concept from a higher level at the current level
10. Idempotent map of a concept

user21820

Oh yes back to logic.

@LastIronStar: I'm now going to explain how we can actually figure out the proof of LEM.

So you can read this part later when you're back.

David Reed

one might mention LEM = tautology

user21820

No.

David Reed

07:44

no?

user21820

LEM is law of excluded middle.

I'm not doing the semantic-completeness theorem now.

David Reed

A or not A is not a tautology?

user21820

It is, but it's not equal.

David Reed

ah yes the = was meant to be read as "is a "

I can see how that might be ambigous

user21820

Lol okay. Let me finish first.

Let me copy the rules again first for easy reference:

18 hours ago, by LastIronStar

1. Repeat:
| A
|---------
| A
2. If-sub
|
|---------
| If A:
|      A.
3. If-repeat
| A
| If B:
|---------
|     A.
4. Implies
| if A:
|     B.
|----------
| A => B.
5. Dual of implies
| A.
| A => B.
|-----------
| B.
6. And-create
| A.
| B.
|-------
| A and B.
7. And-destroy
| A and B.
|---------
| A.
| B.
8. Or-Create
| A.
|---------
| A or B.
| B or A.
9. Or-destroy
| A or B.
| If A:
|     C.
| If B:
|     C.
|---------
| C.
10. not-destroy
| not not A.
|------------
| A.
11. Contradiction
| If A:

Secret

07:48

I still felt like we are missing a not rule. There should be two not rules like
|A or B
|not A
|------
|B

?

user21820

To produce a theorem, we need to write some sentence in the outermost context without doing so before. If you look at the rules, the only way to do such a thing is via either Implies-Intro or Not-Intro.

@Secret No need. You can prove that.

Secret

ah ok

David Reed

you are skirting dangerously close to the notion of completeness there secret

user21820

Anyway let me finish first; this is going to get hard for LastIronStar to read if we keep going on tangents.

Secret

ok

user21820

07:50

7 mins ago, by user21820

@LastIronStar: I'm now going to explain how we can actually figure out the proof of LEM.

2 mins ago, by user21820

To produce a theorem, we need to write some sentence in the outermost context without doing so before. If you look at the rules, the only way to do such a thing is via either Implies-Intro or Not-Intro.

And the desired theorem has main boolean operation "or". How to get it? We can't hope to prove "A" or "not A" separately, as required by Or-Intro.

So it must have been there already somehow.

The desired theorem also does not have "implies" in it. It turns out that every theorem of the form "A implies B" can be proven by proving "B" under the subcontext of "If A:".

So we sort of know the only way to prove "A or not A" is to use Not-Intro.

I can't really be precise here, but Not-Intro is the only rule that lets us get something from nothing.

So we must start with "If not ( A or not A ):" and try to get a contradiction inside if we believe the desired theorem is right.

Of course we know we must use Not-Elim at the end. So we are half done.

Inside we want to prove a contradiction, and naturally we would expect to be able to prove "A or not A" itself. This looks like the same problem we started with, but we have an extra thing that holds in this context. So we can try to see if Or-Intro works.

That leads to "If A:" and contradiction, so "not A" and contradiction. And we are done.

More or less that is how I figure out such proofs.

Secret

hmm, so of all 11 rules, only 2 of them can move up one level of the hierarchy of contexts

and that is what we need to figure out how to prove a theorem

user21820

08:05

Yea.

The general approach is what we will show in the semantic-completeness theorem, and this is just a taste of it for a specific instance.

David Reed

The first system I ever encountered had something like 27 rules

made proving things a breeze, made studying for the exam a nightmare

user21820

@DavidReed With quantifiers? For this system we need 6 more, 2 for each quantifier and 2 for equality.

David Reed

no w/o

user21820

Wow that is kind of silly.

David Reed

no quantifiers or relations

just sentence letters

user21820

08:08

In my opinion propositional logic is best done either with truth tables or some rather minimal system.

If you have many many redundant rules then you're basically doing truth tables along the way.

David Reed

the truth tables were the justification for the rules. As long as the rules are sound doesn't really matter how many you have imo. The more you have the easier is to prove things

user21820

Well yea.

David Reed

exactly

when you study systems as a whole the opposite is quite preferable

symbol wise to--I prefer in that context to define everything in terms of just not, or, exists

user21820

@DavidReed Yes the other extreme is Hilbert-style. Easy to analyze, but impossible to use. I choose the above minimal Fitch-style as a reasonably human-usable system that will not be too painful to analyze.

David Reed

In practice, I prefer to use David style-- which consists of a random assortment of truth tables, sequents, fitch-like rules, and common sense

user21820

08:17

Lol of course that's the easy way. But I have actually made intuitive mistakes many times that I only found when I tried to write Fitch-style. Once on a measure theory exam I thought I solved a problem, only to realize after writing out nearly the whole idea that I could not pull out the desired conclusion from underneath a subcontext...

Whole idea had to be abandoned. But I found and wrote down a correct proof just before the time was up.

It was the usual kind of accidental quantifier switch.

David Reed

yes by common sense I mean that I will immediately accept things like " A or B, not A ---Therefore B" as true without proof

yah quantifiers are tricky in real analysis

I wrote that up on an answer recently

user21820

@DavidReed That for sure. In practice we might as well use propositional tautologies freely.

@mohammadreza: Hello! (Mathematical) logic discussion/inquiry is welcome here. =)

@Secret: Anyway I think I'll show the semantic-completeness theorem when LastIronStar is here as well. More efficient that way haha..

You can try to convince yourself though, that you can perform case analysis.

Secret

ok

David Reed

is semantic completeness theorem a synonym for soundness of system theorem?

user21820

No it's usually taken to mean the converse.

A system is sound iff every theorem it proves is true in every context (or more conventionally every model of the axioms).

A system is semantically complete iff every sentence that is true in every context is a theorem that it proves.

David Reed

08:27

I shall rephrase:

ok nvm

so semantic-completeness theorem is just regular completeness theorem

user21820

Yes, and I only add the adjective to distinguish it from the syntactic-completeness theorem.

David Reed

that should be quite exciting for @Secret

user21820

He actually participated in the short discussion session I held on the incompleteness theorems prior to writing my linked post.

A bit like the wrong order, but oh well.

@DavidReed: Okay I'm going off to do other stuff now. See you next time!

David Reed

ok

user21820

@DavidReed: Oh and if you have lots of free time, here are some puzzles I found that are quite interesting:

David Reed

08:33

I have plenty of free time, I'm going to be short on attention span till early feb unfortunately

for reasons mentioned last night

user21820

chiark.greenend.org.uk/~sgtatham/puzzles

This collection all are designed to be solvable by logical deduction, meaning no luck required.

David Reed

quite a few

user21820

Including Mines, which is a no-luck version of Minesweeper.

David Reed

the 15 puzzle i played religiously as a kid

user21820

I particularly like Tracks and Net[game].

A particularly hard one is Loopy (try the hexagonal grid).

Then there is Madore's word riddles:

madore.org/cgi-bin/madore-cgi-main/puzzle/puzzle1/index

Madore is a logician who invented some ordinal collapsing function!

After a few months of mostly unconscious thinking, I finally managed to solve all of them.

David Reed

08:36

I feel like untangle can be solved using algorithms from graph theory

user21820

There is supposed to be a linear time algorithm! But I don't know it.

And finally, the best of all (but quite time-consuming):

pleasingfungus.com/Manufactoria

David Reed

kind of an oxymoronic site name

user21820

This is essentially a build-your-own Turing machine game in nice kid-friendly format.

Except that kids will hardly be able to solve it.

David Reed

I appreciate the thought man. Thank you

user21820

Okay I'm off have fun hahaha!

=)

David Reed

08:39

I will check them out

goodnight

user21820

Good night!

David Reed

I'll listen to those songs as well

giving my ears a break atm

user21820

Yea sure it's just for fun. And from these you get a peek into my personality.

LastIronStar

11:33

I've tried to prove it for the better part of last hour. @user21820. This is what I've got:

Q := A or ( A => B )  [short-hand]


If not Q:
	not Q.
	If A:
		Q.
	not A.
	If A => B:
		Q.
	not( A => B).

I know I have to show that either A or Q or A => B can be written in the context of not Q. But i'm stuck.

Hint would be helpful

Secret

OMG this is very short!

Let Q be the label for A or ( A implies B )
If not Q:
    If A:
        B
    A implies B
    Q
    not Q
not not Q
Q.

Secret

11:50

Attempted proof that the rules of or is a tautology:

If A:
    A
    A or B
If B:
    B
    A or B
A or B

user21820

@Secret Wrong.

Secret

o wait, I have no way to make B

user21820

Yes.

As I said, you must put more effort into following the rules...

Formal systems are all about rules.

@LastIronStar Hint ah...

You successfully showed "If not Q: not A."

You could then try to show "If not Q: A implies B."

LastIronStar

I see

user21820

@Secret: I'm sure you can do it. Just be careful to follow the rules, but also experiment more with what you can write. Don't be afraid to try everything you can think of (but of course don't get too deeply nested).

LastIronStar

12:03

@user21820 wait are you sure of this?

no typos right?

user21820

Yea looks right to me. The goal is to contradict the "not Q".

LastIronStar

@user21820 the strategy is setup something like follows:

user21820

@LastIronStar And actually you can see from the semantics of "implies" that you ought to be able to do it given what you have already done.

@AbdulMalekAltawekji: Hello! Questions/inquiry about (mathematical) logic are welcome here.

LastIronStar

@user21820 I get what you're saying intuitively in fact, that's why I kept at my proof this long! Let me try again

I'm specifically having trouble seeing how to use rules to write 'If A doesn't imply B then'

user21820

The only way you need to use to prove an implication is via Implies-Intro.

It always works.

LastIronStar

12:10

wait i think i got it

let me write it up

damnit

LastIronStar

12:25

latest iteration:

Q := A or ( A => B )  [short-hand]

If not Q:
	If A:
		Q.
	not A.
	If B:
		If A:
			B.
		A => B.
		Q.
	not B.
	?????
	Q.
not not Q.
Q.

user21820

Everything you wrote there is fine (up to the ??? of course). If you want to get "If not Q: A implies B." you would need to get "If not Q: If A: B.". Are you sure you can't?

If not Q:
	If A:
		Q.
	not A.
	If A:
		???
		B.
	A => B.
	Q.
not not Q.
Q.

LastIronStar

12:44

If not Q:
	If A:
		Q.
	not A.
	If A:
		If not B:
			Q.
		B.
	A => B.
	Q.
Q.

@user21820 ^

11 lines!

user21820

@LastIronStar Why is it your second Q can just pop up from thin air?

LastIronStar

cos of being inside "If A:"

user21820

Oh...

Then okay just add in the not not B and it is fine and you can in fact remove the first "If A:".

LastIronStar

If not Q:
	If A:
		If not B:
			Q.
			not Q.
		not not B.
		B.
	A => B.
	Q.
not not Q.
Q.

user21820

See my solution here which is the same just without those few lines.

LastIronStar

12:52

now? @user21820

11 lines

user21820

Correct.

Great!

LastIronStar

Are Humans as a whole becoming biologically smarter as civilisation is progressing? Or is it like we still haven't filled the bowl of intelligence that we had when we began snowballing into modern humans? What do you think?

user21820

@LastIronStar I don't believe in macro-evolution. And I don't think as a whole we are getting any wiser. We are becoming cleverer at blowing ourselves up.

LastIronStar

but macro-factors are an aggregate of microlevel factors. Are you saying there can't be "more is different" level of selection that happens at species/whole population level?

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic