On Thursday, December 30, 2021 at 2:44:55 PM UTC-5, Mostowski Collapse wrote:
> What if I want to prove:
>
> ALL(x):[Human(x)=>Mortal(x)]

Contrapositive: ALL(x):[~Mortal(x) =>~Human(x)]

> ~Mortal(father(newton))
> ----------------------------------------------------
> ~Human(father(newton))
>

What is 'father(newton)'? Is it mortal or not? Is it human or not? We are not told. It is undefined. As such, we are unable to attach a truth value to either 'Mortal(father(newton))' or 'Human(father(newton))' without any further information.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, December 30, 2021 at 2:49:06 PM UTC-5, Mostowski Collapse wrote:
> Also you invented premisses that I never stated, such as
> Human(newton), or ALL(x):[Human(x)=>Human(father(x))]
> translated to sets.

I assumed you wanted your question to make sense. I suppose I should have known better. Without these additional assumptions, your argument goes nowhere. It is nonsense like your subsequent version here.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Works fine in textbook first order logic.

See also:

∀x(Hx → Mx), ¬Mf(n) entails ¬Hf(n)
https://www.umsu.de/trees/#~6x%28Hx~5Mx%29,~3Mf%28n%29|=~3Hf%28n%29

So you botched DC proof? Made it unusable?

Dan Christensen schrieb am Donnerstag, 30. Dezember 2021 um 22:00:41 UTC+1:
> On Thursday, December 30, 2021 at 2:44:55 PM UTC-5, Mostowski Collapse wrote:
> > What if I want to prove:
> >
> > ALL(x):[Human(x)=>Mortal(x)]
> Contrapositive: ALL(x):[~Mortal(x) =>~Human(x)]
>
> > ~Mortal(father(newton))
> > ----------------------------------------------------
> > ~Human(father(newton))
> >
>
> What is 'father(newton)'? Is it mortal or not? Is it human or not? We are not told. It is undefined. As such, we are unable to attach a truth value to either 'Mortal(father(newton))' or 'Human(father(newton))' without any further information.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, December 30, 2021 at 7:06:42 PM UTC-5, Mostowski Collapse wrote:
> Works fine in textbook first order logic.
>
> See also:
>
> ∀x(Hx → Mx), ¬Mf(n) entails ¬Hf(n)

Another instance of Burse's Paradox!

IIUC given any unary function f with domain D, we can assign a truth value to the unary proposition P(f(n)) even if f(n) is undefined, i.e. if n is not an element of D.

While this may work in philosophy class, it is a definite non-starter in mathematics and in DC Proof. Essentially, for any function f: D --> C, we can only make inferences about f(n) when n is an element of D. Not when f(n) is undefined. Sorry, Jan Burse.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, December 30, 2021 at 7:06:42 PM UTC-5, Mostowski Collapse wrote:
> Works fine in textbook first order logic.
>
> See also:
>
> ∀x(Hx → Mx), ¬Mf(n) entails ¬Hf(n)

Another instance of Burse's Paradox! IIUC it states that, given any unary function f with domain D, we can assign a truth value to the unary proposition P(f(n)) even if f(n) is undefined, i.e. if n is not an element of D.

While this may work in philosophy class, it is a definite non-starter in mathematics and in DC Proof. Essentially, for any function f: D --> C, we can only make inferences about f(n) when n is an element of D. Not when f(n) is undefined. Sorry, Jan Burse.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Its just ordinary FOL. You can also prove it like this in LK:

1. h(f(n)) ⊢ h(f(n)) (ax)
2. m(f(n)) ⊢ m(f(n)) (ax)
3. h(f(n)) ⇒ m(f(n)), h(f(n)) ⊢ m(f(n)) (L⇒, 1)
4. h(f(n)), ∀x(h(x) ⇒ m(x)) ⊢ m(f(n)) (L∀)
5. ∀x(h(x) ⇒ m(x)) ⊢ m(f(n)), ¬h(f(n)) (R¬)
6. ∀x(h(x) ⇒ m(x)), ¬m(f(n)) ⊢ ¬h(f(n)) (L¬)
7. ∀x(h(x) ⇒ m(x)) ∧ ¬m(f(n)) ⊢ ¬h(f(n)) (L∧)
8. ⊢ (∀x(h(x) ⇒ m(x)) ∧ ¬m(f(n))) ⇒ ¬h(f(n)) (R⇒)

http://www.xlog.ch/izytab/moblet/en/docs/18_live/40_bin2021/paste07/package..html

The inference rules are from here:

https://en.wikipedia.org/wiki/Sequent_calculus#Inference_rules

Dan Christensen schrieb am Freitag, 31. Dezember 2021 um 03:55:23 UTC+1:
> On Thursday, December 30, 2021 at 7:06:42 PM UTC-5, Mostowski Collapse wrote:
> > Works fine in textbook first order logic.
> >
> > See also:
> >
> > ∀x(Hx → Mx), ¬Mf(n) entails ¬Hf(n)
> Another instance of Burse's Paradox! IIUC it states that, given any unary function f with domain D, we can assign a truth value to the unary proposition P(f(n)) even if f(n) is undefined, i.e. if n is not an element of D.
>
> While this may work in philosophy class, it is a definite non-starter in mathematics and in DC Proof. Essentially, for any function f: D --> C, we can only make inferences about f(n) when n is an element of D. Not when f(n) is undefined. Sorry, Jan Burse.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Friday, December 31, 2021 at 2:18:51 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Freitag, 31. Dezember 2021 um 03:55:23 UTC+1:
> > On Thursday, December 30, 2021 at 7:06:42 PM UTC-5, Mostowski Collapse wrote:
> > > Works fine in textbook first order logic.
> > >
> > > See also:
> > >
> > > ∀x(Hx → Mx), ¬Mf(n) entails ¬Hf(n)

> > Another instance of Burse's Paradox! IIUC it states that, given any unary function f with domain D, we can assign a truth value to the unary proposition P(f(n)) even if f(n) is undefined, i.e. if n is not an element of D.
> >
> > While this may work in philosophy class, it is a definite non-starter in mathematics and in DC Proof. Essentially, for any function f: D --> C, we can only make inferences about f(n) when n is an element of D. Not when f(n) is undefined. Sorry, Jan Burse.

> Its just ordinary FOL.

Indeed. Maybe this is why so-called mathematical logic (includes ordinary FOL) is not a required course in most pure math programs (e.g. at MIT). A more math-oriented form of logic is required. Sorry, Jan Burse.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen wrote:

> On Friday, December 31, 2021 at 2:18:51 AM UTC-5, Mostowski Collapse
> wrote:
> Indeed. Maybe this is why so-called mathematical logic (includes
> ordinary FOL) is not a required course in most pure math programs (e.g.
> at MIT). A more math-oriented form of logic is required. Sorry, Jan
> Burse.

morone, you capitalists are 100% extreme wankers.

for instance https://www.youtube.com/watch?v=WweefEJgiwY

🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴
🔴🔴🔴🔴🔴🌕🌕🔴🌕🌕🔴🔴🔴🔴🔴
🔴🔴🔴🔴🌕🌕🌕🔴🔴🌕🌕🔴🔴🔴🔴
🔴🔴🔴🌕🌕🌕🌕🔴🔴🔴🌕🌕🔴🔴🔴
🔴🔴🌕🌕🌕🌕🔴🔴🔴🔴🌕🌕🌕🔴🔴
🔴🌕🌕🌕🌕🌕🌕🔴🔴🔴🔴🌕🌕🔴🔴
🔴🔴🌕🌕🔴🌕🌕🌕🔴🔴🔴🌕🌕🌕🔴
🔴🔴🔴🔴🔴🔴🌕🌕🌕🔴🔴🔴🌕🌕🔴
🔴🔴🔴🔴🔴🔴🔴🌕🌕🌕🔴🌕🌕🌕🔴
🔴🔴🔴🔴🌕🔴🔴🔴🌕🌕🌕🌕🌕🔴🔴
🔴🔴🔴🌕🌕🌕🔴🔴🔴🌕🌕🌕🔴🔴🔴
🔴🌕🌕🌕🔴🌕🌕🌕🌕🌕🌕🌕🌕🔴🔴
🔴🌕🌕🔴🔴🔴🌕🌕🌕🔴🔴🌕🌕🔴🔴
🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴🔴