For reference it is being discussed here.

@user21820 can you restate only those formulas with your restate rule inside a block that are in the scope of this block? scope exactly as in the C-blocks scope sense?

by blocks I mean subcontexts

@famesyasd I'm not sure I can parse your question correctly (a lot of prepositional phrases and relative clauses!) but in my post I had 3 restate rules, called "restate" and "→restate" and "∀restate". The first one lets you restate something in the same context. The other two allow you to pull in something from an enclosing context.

yes when you pull something from an enclosing context you can do this iff the formula is in the C-scope of the block, right?

Ah okay that was your question. Yes that's right.

nice

I guess I was overly concise when I wrote "The context of each statement is specified by all the headers that are in effect.".

Haha; I sort of expect people to understand intuitively what a multi-level list means. =)

a have no idea of what a multi-level list means nor did I when I googled it I guess one needs to watch some video with some example of it to udnerstand what that means

@famesyasd I linked from my post to the wikipedia article on that; was it not clear enough?

yup it wasn't

Oops then perhaps I should look for a better explanation.

I didn't udnerstand in in both English and my natural language

lol...

And I commend you on finding such tiny technical details because there is no way a fully precise specification of a Fitch-style natural deduction system can be that short.

In particular, your question gets at the specific meaning of my indented "..." in my rules.

For example, in "→restate" there cannot be intervening lines in that "..." that have lower indentation.

And in "→intro" clearly the same restriction holds.

didn't get the last two lines

please expand by an example

Let me quote the rule:

→restate: If we prove something outside a conditional subcontext, we can restate it inside.

|A.
|...
|If B:
|  ...
|-------
|  [A.]

Valid example:

If A:
  A.
  If B:
    A.

Invalid example:

If A:
  A.
  If B:
If not A:
  If C:
    A.

how did you get the last A there

That's why it's invalid.

first if A is already closed

My point is that I am relying on people to use their common sense so that they will not misuse the rule in the invalid manner above, but technically speaking it all has to be precisely spelt out in a complete formalization.

I'm just saying that your question is about exactly the same thing; you can only drag a deduced statement into a subcontext, not somewhere else.

Makes sense?

yes!

what if you have forall x exists y x > y and then you apply your forall elim to get exists y y > y?

@famesyasd: Also, as noted in my post, in practice you do not explicitly write down any of the sentences permitted by the restate rules, because you can mechanically find them if they are used.

@famesyasd You can only apply forall-elim to an existing object, not an arbitrary variable.

That's why I like the type-checked version of my rules. That rule in particular is:

∀elim: If we prove a ∀-statement, we can apply it to any object of the required type.

|∀x∈S ( P(x) ).
|...
|E∈S.
|...
|--------------- (where E is an object expression)
|P(E).

See, you need to have deduced "E∈S" as well.

mm okay

Note that your example "forall x exists y ( x > y )" is satisfied if the domain is empty, and my variant works for empty structures, unlike most Hilbert-style systems.

@user21820 are we able to conclude from f(3) = 5 that exists y f(y) = 5?

@famesyasd Yup, as long as y is unused in the current context.

Just so that there is no variable shadowing.

okay

@user21820 can one do model theory without ZFC?

@LeakyNun Well it depends a lot on what your choice of foundation is. I think you can do a fair amount of concrete model theory in higher-order arithmetic plus choice. But if you want to have transfinite induction along any well-ordering you're surely going to need higher types than that.

but isn't everything circular?

Specifically? I think it's fair enough to say that higher-order arithmetic (but without choice) is not circular if you interpret it in a certain way.

Not circular in the sense that there is a reasonable real-world interpretation, whether ultimately accurate or not.

Beyond that it's hard to tell.

If you want to be safe and sound, logicians think that ACA is very safe, and ATR is quite safe.

ok so here's the situation with ZFC

we define a model as a set plus some functions plus some conditions

but what is a set, you ask

And ZFC cannot exactly answer in the same way it can answer the 'usual' questions.

Because "set" is not captured by a set.

I mean, we already presupposed ZFC when we work with theories and models, and then we talk about ZFC as a theory?

@LeakyNun Well yes that's what set theorists do. They work within ZFC and prove things about ZFC. Model theory in general has less dependence on ZFC.

You just need a foundational system that can reason about collections and structures in a sufficiently general way.

but we're defining ZFC using ZFC

No ZFC is a computable formal system; you can define it as a particular program (as a theorem generator, or as a proof verifier).

what is a program?

mathematically a program is still a set in ZFC right

No that's only if you already chose ZFC as your foundational system. You don't need anything near ZFC to define ZFC.

You first set up an ideal programing language. To do so, you need to be able to reason about (finite) (say binary) strings, as well as collections of strings, so that you can define what is meant by execution of a program on an input.

So your foundational system MS should be roughly at least ACA.

what is [insert concept of ACA]? isn't that also defined using ACA?

I'm not sure what you mean by that. We have a real-world idea of what an ideal program is like (computer program with extensible memory). We can see (by human intuition) that ACA seems to be sound for that notion. So we start working within ACA, which we can check by using the program we write in the real world to verify ACA (theorem,proof) pairs.

Within ACA, we can then define ZFC. We could also define ACA internally, and that ought to correspond to our real-world notion.

ACA is a set of some axioms like ZFC?

@famesyasd Yeap; ACA basically is PA plus the ability to quantify over sets of naturals, plus the ability to construct any set of natural numbers that is defined by an arithmetical property, then plus induction.

PA are those 5 axioms about natural numbers? 4 about the successor fucntion and the last one is about induction?

@famesyasd More or less, but when I say PA I am always referring to the discrete ordered semi-ring axioms plus induction.

okay

I have to say "plus induction" again because induction is stronger when you have more properties you can induct on, and in ACA since you can quantify over sets of naturals it means that you can also induct on a property that involves such quantification.

Anyway, @LeakyNun, this isn't circular, because we check our ACA proofs by physical hand/computer, but when we literally work within ACA it is governed by the rules of the physical ACA system. Of course we hope that the internal reasoning about strings within ACA is actually true for physical strings, but one is free not to assume that.

but how do you have uncountable models that way?

You don't. ACA does not pretend to know about countable models.

ACA can tell you that if ZFC is consistent then it has a model.

But ACA surely cannot tell you anything about cardinalities.

So if you believe in powersets then you cannot take ACA alone as foundational, because you at least would have the finite iterates of powerset on N.

By the way, ACA does prove Cantor's theorem! If you think about it, it makes sense because there is no arithmetical set (viewed as a set of pairs) that encodes a surjection from N onto the arithmetical sets.

I need to go soon though, so I'll respond next time! See you! =)

(Sorry I made a typo: ACA does not pretend to know about uncountable models.) And I meant it in the 'size' sense, not the 'surjection' sense.