Mathematics - 2018-04-15 (page 2 of 2)

Alessandro Codenotti

22:00

Urgh I don't have the time to think about such a question now, I was expecting something nicer :/

Vrouvrou

>__<

please just a minute i do all the calculus

0celo7

@Semiclassical this is going to be a (in my opinion) interesting talk. I hope the audience can follow

Semiclassical

22:35

good luck

0celo7

@Semiclassical I am currently thinking about how to explain stability in the compact-open Sobolev topology :P

Semiclassical

...good luck :P

0celo7

I'll probably just lie and make it easier than it actually is

user17629

@XanderHenderson I just curious if this possible, since I would like some constructive statement rather that suppose some features

Meow

23:08

What's the most natural definition of current (or distribution) in an algebraic context?

I read that the currents on, say, $\mathbb{C}$, are $D/Dx$ where $D=\mathbb{C}[x,\frac{\partial}{\partial x}]$.

Kasmir Khaan

@LeakyNun hey leaky :D

I got some questions about logic , text me when you back :D

Leaky Nun

@KasmirKhaan hi

Kasmir Khaan

yeeey :D

you have time leaky ?

@LeakyNun Wake up :D

Leaky Nun

@KasmirKhaan sure

Kasmir Khaan

yeey :D

all righty , we started the course with inductivly defined sets

and took an example of natural numbers

that part was ok for me :D

then we did semantics and propositinal logic

this where i got lost a bit :/

Leaky Nun

23:16

I see

Kasmir Khaan

so what is propositions P_i stand for?

Leaky Nun

it's just a variable

(its intended value is either true or false)

Kasmir Khaan

so i can think of it as any statement ?

Leaky Nun

so "proposition" means "assertion" or "claim" right

Kasmir Khaan

which is either 0 or 1 ?

Leaky Nun

23:17

yes

Kasmir Khaan

okay so far so good :D

and we use greek letters

phi and psi for formulas

if i understood this right

Leaky Nun

sure

Kasmir Khaan

something like P_1 ==> P_2 is no longer a proposition

it is a formula now right?

Leaky Nun

not sure

Kasmir Khaan

the book calls those metavariables

Am not sure why

Leaky Nun

23:18

interesting distinction

Kasmir Khaan

hehe

Leaky Nun

I don't really care about how things are called

I just use them

Kasmir Khaan

nice :D

okay you know about the set FORM ?

Leaky Nun

what set form?

Kasmir Khaan

okay so it is not universal ><

well the way the book defined it is

P_i in FORM

"and " "or " " entails" are in form

P_1 in form , P_2 in form, P_1 "and" P_2 in form

or any other operation between em

Leaky Nun

23:21

oh

Kasmir Khaan

what do you call that?

Leaky Nun

the set of well-formed formulas

wait no, it shouldn't have "and"

Kasmir Khaan

okay i think we are on same page now :D

hmm it does in this book

Leaky Nun

whatever, go on

Kasmir Khaan

"TRUE" " False " are also in form

now the claim is this set form is inductlvly defined set

and from that statement i thought i knew what inductivly defiend means but now it seems like I dont

we have elements of this set

Leaky Nun

23:23

btw when you said "entails" you mean "implies"

Kasmir Khaan

yes implies

in this book they use entails as a synonym

Leaky Nun

"entails" is a different thing

Kasmir Khaan

okay

so we have a set of any number of propositions

and some binary operations between them

and we have true and false

how to see that this is an inductivly defined seT?

Leaky Nun

the base case is the propositions and the operations

Kasmir Khaan

okay

Leaky Nun

23:26

the inductive step is "P_1 in FORM and P_2 in FORM => P_1&P_2 in FORM and P_1|P_2 in FORM and P_1->P_2 in FORM"

Kasmir Khaan

so there is nothing to read into there right?

the set being inductivly defined means that we start and we continue

base case , and the case n+1

Leaky Nun

right

you see, what you just said is just induction for the natural numbers

this thing here is induction generalized a billion times

Kasmir Khaan

yes but i dont see the analogy here

aha

what are we unducting upon here?

the props P_i's ?

Leaky Nun

we aren't; this is an inductively defined set which will allow us to do induction

Kasmir Khaan

hmm

Leaky Nun

23:29

so the natural numbers nat are inductively defined as follows:

Kasmir Khaan

eg if we want to compute P_1 "and" P_2 "and" P_3 we can do it inductivly ?

Leaky Nun

inductive definition nat:
| zero : nat
| (n : nat) -> (succ n : nat)

"zero is a nat, and whenever n is a nat succ n is a nat"

and the most important bit

"and nat is the smallest set containing those things", i.e. "every nat is formed this way"

Kasmir Khaan

okay this example makes perfect sense to me

one has to begin and then continues

0 in N

Leaky Nun

and then induction is that for a proposition p(n) of nat, you prove p(zero) and p(n)->p(succ n), and then it gives you p(n) for all nat

Kasmir Khaan

s(n) in N

Leaky Nun

23:32

so if you want to prove that something is true for every well-formed formula

you prove that it is true for the atoms P_1 P_2 ...

Kasmir Khaan

okay how to draw the analogy from natural numvers to the set FORM ?

Leaky Nun

and you also prove that it is true for P_1 and P_2 imply it is true for P_1&P_2 etc

and then induction says it is true for everything in FORM

Kasmir Khaan

seems a bit cryptic at this point =P but lets keep going :D

we use the notation [[ phi ]]

for truth value

Leaky Nun

Structural induction

Structural induction is a proof method that is used in mathematical logic (e.g., in the proof of Łoś' theorem), computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction over natural numbers, and can be further generalized to arbitrary Noetherian induction. Structural recursion is a recursion method bearing the same relationship to structural induction as ordinary recursion bears to ordinary mathematical induction. Structural induction is used to prove that some proposition P(x) holds for all x of some sort of recursively defined structure...

one might call it "structural induction"

Kasmir Khaan

okay ill read that :D

btw we use different notation

Leaky Nun

23:34

do you have any CS / programming background?

they surely help in logic because of their precision

Kasmir Khaan

we put a line

Nope :/ nada

we put a line, and what above it is what we can assume, and below the line, is what we can conclude from what we can assume

Kasmir Khaan

0 in N

it would look like that, we dont need anything to say that 0 is natural number

n in N

Leaky Nun

that isn't "different notation", that's the inference line in Gentzen-style

Kasmir Khaan

s(n) in N

aha okay good that you know that notation :D

Leaky Nun

different from what?

Kasmir Khaan

23:36

because i was planning to send you some exercice i done by hand

Leaky Nun

and the resulting mess is called a 'proof tree'

Kasmir Khaan

haha yes :D

okay am gonna hsow this

[[ "not" phi ]] = "not" [[phi]]

as in truth value ?

those double bar notation is something standard right?

am in the section of semantics now

Leaky Nun

I don't know the standard, but I can understand what you want to say

Kasmir Khaan

okay , here i just follow the defintion

"not" phi := phi ==> 0

[[ phi ==> 0 ]] = [[phi ]] ==> [[0]]

but here where i get comfused

i need to somehow show that i can pull out that "not" symbol

but what i end up with is [[phi ]] ==> [[0]]

Leaky Nun

well what is the truth value of 0?

Kasmir Khaan

23:42

well we use upside down T

for false

i just put 0 so you are with me =p

[[T]] = 1

Leaky Nun

you still haven't answered my question

Kasmir Khaan

the value of 0 is 0

do you want me to email you the notes we are using ?

so it would be easiar to communcate?

Leaky Nun

no need

Kasmir Khaan

okay

Leaky Nun

so replace [[0]] with 0 and you are done

Kasmir Khaan

23:45

i dotn follow why one can do that

pull out that "not " symbol

Leaky Nun

you just said the value of 0 is 0

[[0]] is the value of 0

so [[0]] is 0

Kasmir Khaan

but we dont know the truth value of phi

Leaky Nun

this is called, transitivity of equality haha

you don't need to know it

5 mins ago, by Kasmir Khaan

but what i end up with is [[phi ]] ==> [[0]]

replace and you get [[phi]]->0

i.e. not [[phi]]

so you proved that [[not phi]] = not [[phi]]

Kasmir Khaan

aha right right

what i was thinking about is to remove [[]] from phi

which makes the exercice pointless

but that is not the case here =p

I showed [[phi]] --->0

wich is the same as "not" [[phi]]

Leaky Nun

right

Kasmir Khaan

23:48

the other question is [[ phi <--> psi ]] = [[phi]] <--> [[psi]]

btw ,[[phi]]^A

this is the notation for all of those with brackets

its an interpertation thing

any formula has infinite many interpertations, we A is one of them

but when there is no danger of comfusing we can leave out that A

okay i solved it

Leaky Nun

lol

Kasmir Khaan

what is it leaky ?

Leaky Nun

you solved it yourself

Kasmir Khaan

and ? :D

you surprised?

Leaky Nun

while talking

Kasmir Khaan

23:52

hmm i dont get your point leaky =P

i just did this

Leaky Nun

nvm

Kasmir Khaan

[[ phi --> psi "and" psi --> phi ]]

and divided that

[[phi --> psi ]] "and" [[ psi --> phi ]]

and divided the two smaller pieace

[[phi]] --> [[psi]] "and" [ psi]] --> [[phi ]]

wich is what we needed :D

Leaky Nun

right

Kasmir Khaan

do you have an idea why one studies logic?

i fail to see the big picture of it so far

Leaky Nun

well i like exploring foundations of maths to see how everything is justified

Kasmir Khaan

23:55

nice =P

I really want to be better at proofing things logiclly that is why i took the course

but so far , its something very different from what i expected

Leaky Nun

I see

Kasmir Khaan

okay :D now i need to compute this

[[ "not" ( P_1 "or" P_2) ---> "false" ]]

"not" P_1 "or" P_2

this is the same as P_1 "and" P_2 ---> 0 right?

Leaky Nun

I don't think that's right

Kasmir Khaan

hmm

let me think :D

i mean if we want to negate the statements P_1 or P_2

Transcript for

$Mathematics$ Mathematics