Уважаемые, помогите разобраться с невыводимостью формулы.

[Nastenka90]

Помогите, пожалуйста, установить невыводимость формулы A∨¬A в измененной системе аксиом, состоящей из всех аксиом групп 1-3:
1. 1) A→( B→A )
2)( A →( B →C ) )→(( A →B)→(A →C )

2. 1) A & B →A.
2) A & B →B.
3) ( A →B )→(( A →C )→( A →B & C)).

3. 1) A →A ∨B
2) B →A ∨B
3) ( A →C )→(( B →C )→( A ∨B→C ))
и следующих двух аксиом:
(A →B)→((A →B)→¬A),
A → (¬A→B).

Подскажите хотя бы идею. Заранее огромное спасибо.

[gefest_md]

Нужно интерпретировать формулы на множестве $\left\{0,\ \frac{1}{2},\ 1\right\}$ следующим образом:
1. Если $v(A)\leqslant v(B)$, то $v(A\to B)=1$.
2. Если $v(A)>v(B)$, то $v(A\to B)=v(B)$.
3. Значение $A\,\&\,B$ равно минимальному из значений $A$ и $B$.
4. Значение $A\vee B$ равно максимальному из значений $A$ и $B$.
5. И последнее:$\begin{tabular}{c|c} $A$&\neg A\\\hline 1&0\\ 1/2&0\\ 0&1 \end{tabular}$
(Замечание: 1-4 применяются также в двухзначной логике)
Например, вычисление значения одной из аксиом выглядит так:
$\begin{tabular}{ccccccccccccccccc} (&A&\to&B&)&\to&(&(&A&\to&\neg&B&)&\to&\neg&A&)\\ &1&1&1&&1&&&1&0&0&1&&1&0&1&\\ &1&1/2&1/2&&1&&&1&0&0&1/2&&1&0&1&\\ &1&0&0&&1&&&1&1&1&0&&0&0&1&\\ &1/2&1&1&&1&&&1/2&0&0&1&&1&0&1/2&\\ &1/2&1&1/2&&1&&&1/2&0&0&1/2&&1&0&1/2&\\ &1/2&0&0&&1&&&1/2&1&1&0&&0&0&1/2&\\ &0&1&1&&1&&&0&1&0&1&&1&1&0&\\ &0&1&1/2&&1&&&0&1&0&1/2&&1&1&0&\\ &0&1&0&&1&&&0&1&1&0&&1&1&0&\\ \end{tabular}$

Идея заключается в том, чтобы все аксиомы давали всюду $1$, а формула $\neg A\vee A$ - нет.