Если формула $\phi$ доказывает противоречие $\bot$ тогда у нас есть $\vdash\phi\to\bot$?
Я пытаюсь научить себя логике с помощью «Дружественного введения в математическую логику» Лири и Кристиансена.
Он сосредоточен на формулах в том смысле, что аксиомы не обязательно являются предложениями.
Правила интерференции, применяемые в этой книге, - это PC (пропозициональное следствие) и правило квантора QR, утверждающее, что от$\psi\to\phi$ мы можем сделать вывод $\psi\to\forall x\phi$ если $x$ не бесплатно в $\psi$.
Позволять $\mathcal{L}$ быть языком первого порядка, пусть $\bot$ обозначить некоторые $\mathcal{L}$-предложение формы $\psi\wedge\neg\psi$ и разреши $\phi$ быть $\mathcal{L}$-формула.
потом $\Sigma:=\left\{ \phi\right\} $ по определению несовместимо, если есть вывод из $\Sigma$ к $\bot$.
Теперь мой вопрос:
Если $\left\{ \phi\right\} $ непоследовательно, то можно доказать, что также: $\vdash\phi\to\bot$?
Мне ясно, что ответ положительный, если $\phi$ это предложение, потому что тогда мы можем применить теорему дедукции.
А вдруг $\phi$ это не приговор?
Моя попытка:
Если $\tilde{\phi}$ обозначает универсальное замыкание $\phi$ тогда $\left\{ \tilde{\phi}\right\} \vdash\phi$ так что по транзитивности $\vdash$ у нас есть $\left\{ \tilde{\phi}\right\} \vdash\bot$ и применяя теорему дедукции, имеем $\vdash\tilde{\phi}\to\bot$.
Но это только переносит проблему на другой вопрос:
Если есть вычет $\vdash\tilde{\phi}\to\bot$ тогда есть еще вычет $\vdash\phi\to\bot$?
Заранее благодарим вас и приносим свои извинения, если этот вопрос повторяется.
Ответы
Я не читал книгу Лири и Кристиансена, но сейчас читаю «Введение в математическую логику» Мендельсона, так что надеюсь, что смогу ответить на ваш первый вопрос.
Что касается вашего первого вопроса, который гласит: «Если формула ϕ (являющаяся ϕ: ψ ∧ ¬ ψ) доказывает противоречие ⊥, то имеем ли мы ϕ → ⊥?» Я могу ответить: по сути, формула, которая утверждает ψ ∧ ¬ ψ, заставит нас сделать вывод ⊥, эта (ψ ∧ ¬ ψ) → ⊥ формула является теоремой, вот доказательство формулы с использованием правил естественного вывода:
1) ψ ∧ ¬ ψ - предположение
2) ψ - правило E∧ в 1
3) ¬ ψ - правило E∧ в 1
4) ⊥ - в 2,3
5) (ψ ∧ ¬ ψ) → ⊥ - правило I → в 1,4
Если мы посмотрим на таблицу истинности ψ ∧ ¬ ψ, все значения ложны, это означает, что не только (ψ ∧ ¬ ψ) → ⊥ является тавтологией, но также (ψ ∧ ¬ ψ) → X (где X - произвольная формула) является тавтологией. Если формула доказывает противоречие, вы должны проверить все формулы.
Что касается вашего второго вопроса, я недостаточно уверен, чтобы дать ответ, я сейчас читаю вторую главу книги Мендельсона (логика первого порядка), поэтому я разделяю ваши сомнения.