@user638203 Of course. It's impossible to write them if I had to explain at a beginner's level, since it would become a few hundred pages. Logic isn't a shallow subject. In most of my posts I assume familiarity with basic logic, which includes a full deductive system for first-order logic. So you should ask here if you don't understand something.

I have to say that propositional logic isn't anywhere near first-order logic, because truth tables are often used as a crutch, which must be discarded when moving to first-order logic. So if you want to learn logic, you must really learn a deductive system.

I'm biased, but I recommend the one I describe here, which I think is the easiest to use in practice. Other styles (Hilbert-style, sequent-style, tableaux-style) are unintuitive or infeasible beyond toy examples.

Another Fitch-style deductive system that you can try is ProofMood. Note that it's for a slightly different kind of first-order logic, so it's incompatible. (It permits you to prove "∃x ( x=x )" whereas mine does not.)

Whichever system you prefer, you can test whether you know propositional logic by doing the following exercises:

(Standard precedence rules apply; from highest to lowest: not, and, or, implies.)

Whether you use ProofMood or my variant, you can post your attempts here if you want feedback.

@user21820 can we continue?

@famesyasd Sure.

So the question is what you want to have. I personally want to have a universal type and the type of all types, and I prefer strict typing (i.e. cannot use "∈S" unless S is a type in the current context). So in my world, the type R = { x : x∈type ?∧ x∉x } is constructible, and we can prove that R∈R ≡ R∉R and hence R∈R ≡ null, which shows that R does not have boolean membership.

But I won't know what you want; you'll have to tell me. =)

so for example you can only prove that forall A != vn exists single b forall x x in b iff forall s in A x in s

and from that conclude that forall A != vn forall x x in bigcap A iff forall s in A x in s

or you could do that even without anything special

or I forgot why you couldn't do that

ah right, formulas will be ill-defined

so I guess the first approach is to rework some definitio of formulas or soemthing so that formulas won't be ill-defined even with this type of partial functional symbols right?

@user21820 alright, let's start with the first approach and then maybe second

Yes to both questions, more or less. You just have to prove "∀x[1..k]∈S[1..k] ∃!y∈T ( φ(x[1..k],y) )", and then you can introduce a new function-symbol f with input types S[1..k] and output type T. And we indeed need modify the rules for well-formed expressions so that we only use "f(x[1..k])" in a context where we know x[1..k]∈S[1..k].

okay so how do we modify rules? (I probably won't like this xD)

Of course, the axiom we add is also restricted to the domain: "∀x[1..k]∈S[1..k] ( φ(x[1..k],f(x[1..k])) )".

@famesyasd Well, it's of course a little messy. =)

you said of course to what? that I won't like it? xD

I already don't like this xD

@famesyasd No just of course we need to change the added axiom, in case it wasn't obvious.

okay, continue

@famesyasd But why? All mathematicians do it, even if they don't realize it.

Nobody ever writes things like "f(-1)" if the domain of f is N.

And they might consider it meaningless or malformed.

It's still quite clean in Fitch-style. You just have to capture the expression forming rules in Fitch-style itself, rather than separately as in conventional first-order logic.

alright so how do we modify it

For precision, I'll use "A ; ... ; B ⊢ C ; ... ; D" to mean that if you have deduced A,...,B in the current context then you can deduce C,...,D as well.

@famesyasd With a yell that strikes terror into your foes.

xD

YOL... (yell out loud)

heh

For example ⇒elim is ( A ; A⇒B ⊢ B ) and ⇒intro is ( ( A ⊢ B ) ⊢ A⇒B ).

We adopt the standard type-theory notation, and capture the expression forming rules as follows:

A : bool ⊢ ¬A : bool

A,B : bool ⊢ A∧B , A∨B , A⇒B : bool

(where "A,B : S" is short for "A : S ; B : S")

So far this is as usual.

Now add the following rules to capture strict typing for function/predicate-symbols:

f : func(S,T) ; x : S ⊢ f(x) : T.

f : func(S,bool) ; x : S ⊢ f(x) : bool.

And similarly for higher number of inputs.

These rules force us to prove that the thing we want to stick into a function/predicate-symbol is actually in the domain, before we stick it in.

Naturally, when we introduce a new symbol we must also add a typing 'axiom' (commonly called a typing judgement). Namely, if you prove "∀x[1..k]∈S[1..k] ∃!y∈T ( φ(x[1..k],y) )", then you can introduce a new function-symbol f and add the axiom "f : func(S[1..k],T)" and the rule "f : func(S[1..k],T) ; x[1..k] : S[1..k] ⊢ f(x[1..k]) : T".

This technique of overlaying a type-system on top of a standard first-order system is not new; it's used in Mizar, which is a computer proof assistant with one of the largest libraries, which is in fact because having such a type-system and being human-readable makes Mizar user-friendly enough for large amounts of mathematics to be written in it. Mizar's underlying foundation is actually ZFC plus Grothendieck universes.

But I'm not saying that I'm describing Mizar's type system; I'm just showing how we can enforce strict typing in a clean fashion without really disturbing the underlying system.

Oh I forgot one more rule:

x∈S ⊢ x : S.

that's it?

@famesyasd: We're more or less done; the key is simply to replace the syntactic rules by inference rules. In standard first-order logic, we have syntax rules to govern well-formed expressions, and deductive rules to govern what well-formed formulae we can deduce. Here, we just have one set of rules to govern both simultaneously.

For completeness, note that we can capture subcontexts in the same fashion by the following rule:

A : bool ⊢ ( A ⊢ A ).

So that's about it.

syntactic rules are like ⇒elim?

⇒elim is a deductive rule in standard FOL.

Syntactic rules are those that tell you recursively what are well-formed formulae.

Which in standard FOL are completely separate from deductive rules.

okay

There are advantages to standard FOL. You can take any wff Q over a given language L and ask whether it is satisfiable (in some L-structure).

Once you move syntactic rules into the deductive system itself, as I showed above, then what are wffs now is dependent on the axioms as well.

This is perfectly fine if we're using a fixed system (as our foundation for mathematics).

But of course it's no longer easy to analyze systems of this kind in general.

In short, strict typing is good for practical mathematics, but harder to analyze.

@famesyasd: Do you get it?

@user21820 this includes what you was talking about earlier right?

@user21820 that is, here

@user21820 and here

@famesyasd Yes. The rule here captures fully the English "with input types S[1..k] and output type T".

@user21820 so type is not necessarilty a set?

@famesyasd Yes it's not necessarily a set.

alright so I don't get how do I use it then if all my axioms about sets lol

for example I can easily prove that forall x != (the empty set) exists y P(x,y)

how do I turn that into a type

yeah right but that essentially only allows me to create functions

what about function symbols

like in the upper example forall x != 0

x != (the empty set)

I have proved for every set, excluding the empty one

@famesyasd Ah so you want more than functions. Well then you need to have rules for type specification.

yeah I want to handle both bigcap A, and f(x) from functions

Nice; you've a good sense of ambition. =D

xD

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

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

For example, { x : x≠∅ } is the type of all objects other than ∅.

→ 3 messages moved to ­Trash

I deleted it because it's wrong anyway; I miswrote. Here Q is a 1-parameter statement, namely we have previously deduced ( x : obj ⊢ Q(x) : bool ).

Then we get the above two rules, which essentially allow us to create the type corresponding to the property Q.

Note that you cannot ask membership in a type, unlike membership in a set.

You can only recognize membership when you've proven it.

And as you probably know, function-symbols you create this way are not functions in ZFC, so the axioms for ZFC functions don't apply, and I would personally not use "func(...)" to denote its type.

Yes to both.

Away for a while.

okay

Back.

can I unite neg elim neg intro into single A; B ∧ ¬B ⊢ ¬A?

@famesyasd Yes, and might as well ( A ; B ; ¬B ⊢ ¬A ). But there is a severe disadvantage in practice.

Sometimes when you perform a proof by contradiction, under the assumption to be proven false you have a great many cases. In each case you may reach a different contradiction. So if you have a dedicated "⊥" symbol you can happily use ∨elim to get the final contradiction. If you don't, then you have to explicitly use some "C∧¬C" in every case.

@user21820 "f : func(S,T) ; x : S ⊢ f(x) : T." what are f,x f(x) here?

f,x are variables?

yeah, they should be some variables

I'm more interested in what f(x) supposed to mean

@famesyasd Actually f,x,S,T can be any strings with matching brackets, which may be variables or expressions.

aaaaaa

1)

Or rubbish. But you won't be able to use the rule on rubbish because you won't be able to prove rubbish.

matching brackets?

what's this?

by expression do you essentially mean term?

Matching brackets means that every "(" corresponds to some later ")" and the string between them must have matching brackets.

expression = object expression = term?

Yes "term", but I avoid that terminology when I'm not doing ordinary FOL, as people have already reserved that term "term".

okay

most importantly

what is f(x)

f + "(" + x + ")".

so it's just a string

not a functional symbol, not anything?

In practice, every function-symbol is a string, isn't it?

So when you introduce a new function-symbol f, the rule effectively says you can write f+"("+x+")" only in a context where x is in the defined domain of f.

oh nvm

Do you get it, or should I make it program-precise?

I got confused with the function notation f(x)

and how do you deal with the function f(x)?

do you turn the function into a partial function symbol?

@famesyasd Yes that's indeed how we must do it, if we want to share the rules.

No point having one set of rules for (partial-)function-symbols and another for function objects when the latter can be subsumed by the former.

okay, I got the hang on the rules, I'll get the hang on the axiom in 5 minutes then I'll think about that function - function symbols conversion and how to apply them (rules)

@user21820 have you read "The seven virtues of simple type theory"?

@famesyasd Sounds familiar. Note that what I've described goes beyond standard type theory, because objects are not tied to a single type. For example if we deduce that x∈S and x∈T we can conclude x:S and x:T too.

Whereas in standard type theory you can only introduce an object with a fixed type, so it's much less flexible.

oh, right

I spend a couple of days (3-4) reading some books trying to get into type theory but man this is hard

unfortunately I could not get a single virtue of it xD

and also it seems that it is not studied at math departments, right? no one even mentions it

Lol. I don't recommend standard type theory because of the above reason; I don't like the notion that an object has a single fixed type. That also makes reasoning cumbersome.

you mean simple type theory?

Even dependent type theory is still super cumbersome.

could think of it as a class inheriting from a bunch of other classes in a programming language maybe?

@famesyasd I don't know anyone in my university's Maths department that knows it, except for one PhD student who agreed with me that many things just can't be done in a natural way. The only professor in the CS department that knows Coq (based on CoC, which extends dependent type theory with universes and inductive definitions) doesn't have the mathematical background to understand the mathematics behind type theory.

@user525966 Yes you can think of simple type theory as concerning classes in a programming language like Java.

The thing is that mathematics involves reasoning and not just structures and computation, so what is sufficient for programmers isn't sufficient for us.

@famesyasd - FWIW type theories are a super big deal in the math departments of Cambridge and CMU. So it's not purely a CS curiosity.

@MaliceVidrine what is FWIW? I typed it into google and it brought HoTT

@famesyasd For What It's Worth

lol

lol

lol

Am I missing something?

Just woke up to see the "FWIW type theory" interpretation, and was amused.

and indeed it seems that I can't deduce that "forall x in R Triv_R>0(x) = 0" or that "¬forall x in R Triv_R>0(x) = 0" but the only thing preventing me from doing that is precisely the axiom that forall "x in R>0 Triv_R>(x) = 0" and not the typing rules. Moreover I can introduce the "ill-defined" formula "forall x (Triv_R>0(x) = 0 or ¬Triv_R>0(x) = 0) but I can't use it any way so there's no harm in that. So what's the point of the typing rules?

tldr; I thought that the problem with the partial defined function symbols was with ill-defined formulas but it seems now that the only axiom forall x[1..k] in S[1..k] phi[x,f(x)] (forall x in R>0 Triv(x) = 0) is enough to preven me from deducing them. No type-checking required. Or am I missing something or maybe there is other reason?

@famesyasd Please use brackets as it's ambiguous without. The point of the typing rules is to prevent meaningless statements such as "forall x in R ( 1/(1/x) ≠ x ⇒ x = 0 ), which cannot be prevented by the restricted axioms alone.

Similarly, if you define a function f in func(N,N), it is meaningless to state "f(1/2) = 0 ∨ f(1/2) ≠ 0".

This is what we call "junk theorems".

@user21820 but how do I construct formulas now? what prevents me from using lem to get "f(1/2) = 0 ∨ f(1/2) ≠ 0" statement?

The rules here and here make it impossible to prove LEM for meaningless statements, because you can create a conditional subcontext only using a boolean expression.

why do I need to prove LEM now

You said "using lem to get ...". I'm saying "you cannot use LEM to get ..."

LEM was " for any sentence A in FOL you can introduce A or not A in any block"

now it formulates differently?

or the notion of sentence has changed

Emphasis on "replace".

In particular, you'll be unable to prove that "f(1/2)" has a type, namely you cannot prove any statement of the form "f(1/2) : S".

So you'll be unable to prove "f(1/2) = 0 : bool".

This is what strict typing truly means. "f(1/2)" is not well-typed (i.e. fails type-checking).

with what rule could I prove that "f(1/2) = 0 : bool"?

x : S, y : T ⊢ x = y : bool?

and LEM now says that if A : bool ⊢ A or not A, correct?

Yes indeed.

Got to go, but you seem to be getting the idea. =)

yeah I do lol

the only thing I miss

is the first rule

f here = function symbol?

because if it's a term then f(x) is what????

it should be a function symbol so that f(x) is a term

@famesyasd No f here is just a string. Remember, the only way we can use this rule is if we manage to prove "f : func(S,T)", and the other rules are supposed to ensure that we can only do so if the string f really refers to a function from S to T.

These rules are not 100% precise, just like when we write "A∧B" but actually mean A+"∧"+B or something like that.

And we often ignore the issue that we may need additional brackets.

in the second rule

"f : func(S[1..k],T) ; x[1..k] : S[1..k] ⊢ f(x[1..k]) : T".

"f" here is only our function symbol right?

When I wrote that, the rule is supposed to apply in general. For instance "f : func([S,T],U) ; x : S ; y : T ⊢ f([x,y]) : T", if we use square brackets to denote tuples. I didn't want to get into the details because they aren't really important, but you'd have to decide how exactly you want to allow multiple inputs to be captured syntactically.

If you wish you can choose to add individualized rules for each function-symbol you introduce, as you suggested here.

@user21820 and here have you forgot to mention that we also add "∀x[1..k]∈S[1..k] φ(x[1..k],f(x[1..k]) " and also "∀x[1..k]∈S[1..k] forall y ∈ T if φ(x[1..k],y) then y = f(x[1..k]"

I see

@famesyasd We don't need the latter, because if you have already proven the uniqueness statement, you can deduce it later.

but we add "∀x[1..k]∈S[1..k] φ(x[1..k],f(x[1..k]) "?

Yep I did say here, but I know it's messy in here.

Anyway really got to go. See you!

bye!

actually this is super nice lol!!!