Получение Cube(a) из Cube(a) ‹-› a = a (Fitch)

Я пытаюсь что-то доказать в Fitch и застрял на одном шаге, у меня есть:

1.  Cube(a) <-> a = a

и я хочу получить 2. Cube(a) из этого.

Я знаю, что это возможно, потому что я могу использовать Ana Con для 2. и выбрать 1. в качестве предпосылки, и он говорит, что это действительно.
Кто-нибудь может сказать мне, как это сделать без использования Ana Con?


computer-science first-order-logic fitch-proofs
person Aerus    schedule 30.01.2011    source источник
comment
cstheory.stackexchange.com здесь может быть лучше   -  person Andrey    schedule 30.01.2011
comment
Хм, хорошо, я колебался, чтобы поставить его туда, но в конце концов решил не делать этого. Поскольку я не думаю, что смогу переместить это, мне просто удалить его и открыть там новое?   -  person Aerus    schedule 30.01.2011
comment
@Andrey: cstheory предназначена для вопросов исследовательского уровня в теоретической информатике. Уровень исследования означает, грубо говоря, вопросы, которые могут обсуждаться между двумя профессорами или между аспирантами, работающими над докторской диссертацией, но обычно не между профессором и типичным студентом бакалавриата. Пожалуйста, не перенаправляйте нам вопросы по программированию, они не относятся к теме cstheory. Спасибо.   -  person Kaveh    schedule 31.01.2011
comment
ps: теоретические вопросы не исследовательского уровня следует перенаправлять на Math.SE, а не на cstheory.   -  person Kaveh    schedule 31.01.2011
comment
Все, что вам нужно сделать в следующей строке, это ввести тождество a=a. Строка после этого — это биусловное исключение с использованием этих двух строк, которые дают вам Cube(a).   -  person Frank Hubeny    schedule 24.11.2018

Ответы (1)


arrow_upward
2
arrow_downward

(У меня нет копии Fitch, и я никогда ею не пользовался, так что отнеситесь к этому с долей скептицизма. Но я почти уверен, что это правильно.)

Сначала получите просто «a=a», используя =Intro. (Вам не нужны какие-либо предпосылки.) Затем возьмите это плюс 1. и примените ‹->Elim, чтобы получить Cube(a).

person Gareth McCaughan    schedule 15.02.2011