Импликация — это не выводимость. Это логическое следование. Определяемое соответствующими аксиомами логики.
И не надо городить вереницу "выводимостей". Формула
![$6\mid a$ $6\mid a$](https://dxdy-04.korotkov.co.uk/f/3/d/4/3d4a4edff712dacf5c8424dc4c0a035982.png)
означает, что число
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
делится на
![$6$ $6$](https://dxdy-04.korotkov.co.uk/f/3/2/7/327c36301dc71617dc7032f8ce30b23682.png)
, а не какую-то выводимость. Соответственно, формула
![$\forall a(6\mid a\rightarrow 3\mid a)$ $\forall a(6\mid a\rightarrow 3\mid a)$](https://dxdy-02.korotkov.co.uk/f/d/3/2/d328c6548df2589232e36f875bd7d47282.png)
означает, что если (произвольно взятое) число
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
делится на
![$6$ $6$](https://dxdy-04.korotkov.co.uk/f/3/2/7/327c36301dc71617dc7032f8ce30b23682.png)
, то оно делится и на
![$3$ $3$](https://dxdy-02.korotkov.co.uk/f/5/d/c/5dc642f297e291cfdde8982599601d7e82.png)
. Все эти формулы принадлежат предметной теории и никакой выводимости не предполагают, поскольку понятие выводимости принадлежит метатеории.
Соответственно, в метатеории формула
![$\vdash\forall a(6\mid a\rightarrow 3\mid a)$ $\vdash\forall a(6\mid a\rightarrow 3\mid a)$](https://dxdy-03.korotkov.co.uk/f/2/d/a/2daca17a75afac096c4920b90e2abfeb82.png)
означает, что высказывание "если (произвольно взятое) число
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
делится на
![$6$ $6$](https://dxdy-04.korotkov.co.uk/f/3/2/7/327c36301dc71617dc7032f8ce30b23682.png)
, то оно делится и на
![$3$ $3$](https://dxdy-02.korotkov.co.uk/f/5/d/c/5dc642f297e291cfdde8982599601d7e82.png)
" выводимо из аксиом предметной теории.